From 72bb9beb49325da02b98311d0e6f56b1fd11373e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 26 Sep 2021 16:45:30 -0400
Subject: [PATCH] f_equiv: do syntactic matching before attemtping reflexivity

---
 theories/tactics.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 6869a168..7097ce22 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -413,7 +413,9 @@ Ltac f_equiv :=
   | H : _ ?f ?g |- ?R (?f ?x) (?g ?x) => solve [simple apply H]
   | H : _ ?f ?g |- ?R (?f ?x ?y) (?g ?x ?y) => solve [simple apply H]
   end;
-  try simple apply reflexivity.
+  (* Only try reflexivity if the terms are syntactically equal. This avoids
+     very expensive failing unification. *)
+  try match goal with  |- _ ?x ?x => simple apply reflexivity end.
 Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
 
 (** The tactic [solve_proper_unfold] unfolds the first head symbol, so that
-- 
GitLab