Commit e9f14405 authored by Robbert Krebbers's avatar Robbert Krebbers

Add some type annotations to potentially ambiguous cases.

parent 0f11453a
Pipeline #5680 passed with stages
in 7 minutes and 12 seconds
...@@ -208,7 +208,7 @@ Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b. ...@@ -208,7 +208,7 @@ Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed. Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
Global Instance auth_frag_sep_homomorphism : Global Instance auth_frag_sep_homomorphism :
MonoidHomomorphism op op () (Auth None). MonoidHomomorphism op op () (@Auth A None).
Proof. by split; [split; try apply _|]. Qed. Proof. by split; [split; try apply _|]. Qed.
Lemma auth_both_op a b : Auth (Excl' a) b a b. Lemma auth_both_op a b : Auth (Excl' a) b a b.
......
...@@ -25,7 +25,7 @@ Section ofe. ...@@ -25,7 +25,7 @@ Section ofe.
by destruct (decide _) as [[]|]. by destruct (decide _) as [[]|].
Qed. Qed.
Global Instance ofe_fun_insert_proper x : Global Instance ofe_fun_insert_proper x :
Proper (() ==> () ==> ()) (ofe_fun_insert x) := ne_proper_2 _. Proper (() ==> () ==> ()) (ofe_fun_insert (B:=B) x) := ne_proper_2 _.
Lemma ofe_fun_lookup_insert f x y : (ofe_fun_insert x y f) x = y. Lemma ofe_fun_lookup_insert f x y : (ofe_fun_insert x y f) x = y.
Proof. Proof.
......
...@@ -7,6 +7,7 @@ Set Default Proof Using "Type". ...@@ -7,6 +7,7 @@ Set Default Proof Using "Type".
Section cofe. Section cofe.
Context `{Countable K} {A : ofeT}. Context `{Countable K} {A : ofeT}.
Implicit Types m : gmap K A. Implicit Types m : gmap K A.
Implicit Types i : K.
Instance gmap_dist : Dist (gmap K A) := λ n m1 m2, Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
i, m1 !! i {n} m2 !! i. i, m1 !! i {n} m2 !! i.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment