From 24b358206844fbbefa585ca726df6c0011bb447e 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.

---
 theories/base.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 5ff6bee7..ddbf6334 100644
--- a/theories/base.v
+++ b/theories/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