From 046dfe312207d09e1fcbf72dee204be3694195f1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 1 Mar 2017 20:15:51 +0100
Subject: [PATCH] speed up f_equiv by doing reflexivity less often
---
theories/list.v | 2 +-
theories/tactics.v | 1 -
2 files changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/list.v b/theories/list.v
index 2de2b7b5..36f0173d 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3113,7 +3113,7 @@ Section mapM.
(∀ x y, f y = Some x → y = g x) → mapM f k = Some l → k = g <$> l.
Proof.
intros Hgf. revert l; induction k as [|??]; intros [|??] ?;
- simplify_option_eq; f_equiv; eauto.
+ simplify_option_eq; try f_equiv; eauto.
Qed.
End mapM.
diff --git a/theories/tactics.v b/theories/tactics.v
index 5c1143aa..250f8651 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -272,7 +272,6 @@ when having [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], it will
favor the second because the relation (dist) stays the same. *)
Ltac f_equiv :=
match goal with
- | _ => reflexivity
| |- pointwise_relation _ _ _ _ => intros ?
(* We support matches on both sides, *if* they concern the same variable, or
variables in some relation. *)
--
GitLab