Skip to content
Snippets Groups Projects
Commit b36ebb93 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix warnings.

parent 07ba9c07
No related branches found
No related tags found
No related merge requests found
Pipeline #33521 passed
...@@ -17,6 +17,7 @@ Record lrel Σ := LRel { ...@@ -17,6 +17,7 @@ Record lrel Σ := LRel {
}. }.
Arguments LRel {_} _%I {_}. Arguments LRel {_} _%I {_}.
Arguments lrel_car {_} _ _ _ : simpl never. Arguments lrel_car {_} _ _ _ : simpl never.
Declare Scope lrel_scope.
Bind Scope lrel_scope with lrel. Bind Scope lrel_scope with lrel.
Delimit Scope lrel_scope with lrel. Delimit Scope lrel_scope with lrel.
Existing Instance lrel_persistent. Existing Instance lrel_persistent.
......
...@@ -61,6 +61,7 @@ Definition unop_bool_res_type (op : un_op) : option type := ...@@ -61,6 +61,7 @@ Definition unop_bool_res_type (op : un_op) : option type :=
| _ => None | _ => None
end. end.
Declare Scope FType_scope.
Delimit Scope FType_scope with ty. Delimit Scope FType_scope with ty.
Bind Scope FType_scope with type. Bind Scope FType_scope with type.
Notation "()" := TUnit : FType_scope. Notation "()" := TUnit : FType_scope.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment