From e9f144053e657ae5873dfd738f1111d70d7693b3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 29 Nov 2017 19:47:48 +0100
Subject: [PATCH] Add some type annotations to potentially ambiguous cases.

---
 theories/algebra/auth.v      | 2 +-
 theories/algebra/functions.v | 2 +-
 theories/algebra/gmap.v      | 1 +
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 992400cac..87b5a7cc7 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -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.
 
 Global Instance auth_frag_sep_homomorphism :
-  MonoidHomomorphism op op (≡) (Auth None).
+  MonoidHomomorphism op op (≡) (@Auth A None).
 Proof. by split; [split; try apply _|]. Qed.
 
 Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index a4c6a03a7..a0fd519b0 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -25,7 +25,7 @@ Section ofe.
     by destruct (decide _) as [[]|].
   Qed.
   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.
   Proof.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index a09b287e8..b9a995537 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -7,6 +7,7 @@ Set Default Proof Using "Type".
 Section cofe.
 Context `{Countable K} {A : ofeT}.
 Implicit Types m : gmap K A.
+Implicit Types i : K.
 
 Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
   ∀ i, m1 !! i ≡{n}≡ m2 !! i.
-- 
GitLab