From 752d27aa009ab2a51d7bd5fe5ecf9f39efaecce3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Jan 2016 01:27:07 +0100
Subject: [PATCH] Hints for reflexivity also on goals that are not identical.

---
 modures/cmra.v | 2 +-
 modures/cofe.v | 2 +-
 modures/ra.v   | 2 +-
 prelude/base.v | 4 ++--
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/modures/cmra.v b/modures/cmra.v
index 234f9a1ec..a9c55a7bc 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -8,7 +8,7 @@ Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅
 Notation "x ≼{ n } y" := (includedN n x y)
   (at level 70, format "x  ≼{ n }  y") : C_scope.
 Instance: Params (@includedN) 4.
-Hint Extern 0 (?x ≼{_} ?x) => reflexivity.
+Hint Extern 0 (?x ≼{_} ?y) => reflexivity.
 
 Record CMRAMixin A
     `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
diff --git a/modures/cofe.v b/modures/cofe.v
index b508eb45f..5f1e2a4c3 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -5,7 +5,7 @@ Class Dist A := dist : nat → relation A.
 Instance: Params (@dist) 3.
 Notation "x ={ n }= y" := (dist n x y)
   (at level 70, n at next level, format "x  ={ n }=  y").
-Hint Extern 0 (?x ={_}= ?x) => reflexivity.
+Hint Extern 0 (?x ={_}= ?y) => reflexivity.
 Hint Extern 0 (_ ={_}= _) => symmetry; assumption.
 
 Tactic Notation "cofe_subst" ident(x) :=
diff --git a/modures/ra.v b/modures/ra.v
index ad6ce17fe..a6cf97ee0 100644
--- a/modures/ra.v
+++ b/modures/ra.v
@@ -16,7 +16,7 @@ Notation "(â‹…)" := op (only parsing) : C_scope.
 Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : C_scope.
 Notation "(≼)" := included (only parsing) : C_scope.
-Hint Extern 0 (?x ≼ ?x) => reflexivity.
+Hint Extern 0 (?x ≼ ?y) => reflexivity.
 Instance: Params (@included) 3.
 
 Class Minus (A : Type) := minus : A → A → A.
diff --git a/prelude/base.v b/prelude/base.v
index 5ff6bee7b..ddbf6334f 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -209,9 +209,9 @@ Instance: Params (@equiv) 2.
 (for types that have an [Equiv] instance) rather than the standard Leibniz
 equality. *)
 Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3.
-Hint Extern 0 (_ ≡ _) => reflexivity.
+Hint Extern 0 (?x ≡ ?y) => reflexivity.
 Hint Extern 0 (_ ≡ _) => symmetry; assumption.
-Hint Extern 0 (_ ≡{_} _) => reflexivity.
+Hint Extern 0 (?x ≡{_} ?y) => reflexivity.
 Hint Extern 0 (_ ≡{_} _) => symmetry; assumption.
 
 (** ** Operations on collections *)
-- 
GitLab