From e9e6e220cf088d444ed42db4c953c774e74423dc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 13 Dec 2019 17:02:22 +0100
Subject: [PATCH] Mode checking works, these were agressive unifications

That should not be allowed
---
 theories/algebra/gmap.v | 2 +-
 theories/algebra/list.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index db8e78d06..969801c70 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -49,7 +49,7 @@ Global Instance lookup_ne k :
 Proof. by intros m1 m2. Qed.
 Global Instance lookup_proper k :
   Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _.
-Global Instance alter_ne f k n :
+Global Instance alter_ne (f : A → A) (k : K) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k).
 Proof.
   intros ? m m' Hm k'.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index c39d29610..e8a433af8 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -340,13 +340,13 @@ Section properties.
     rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
   Qed.
 
-  Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
+  Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡@{list A} {[ i := core x ]}.
   Proof.
     rewrite /singletonM /list_singletonM.
     by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ∅).
   Qed.
   Lemma list_op_singletonM i (x y : A) :
-    {[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
+    {[ i := x ]} ⋅ {[ i := y ]} ≡@{list A} {[ i := x ⋅ y ]}.
   Proof.
     rewrite /singletonM /list_singletonM /=.
     induction i; constructor; rewrite ?left_id; auto.
-- 
GitLab