From 58e2c6082b3f58b36a2f5b1ccbe9e16c3bb38d32 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Sat, 11 Nov 2017 12:29:41 +0100
Subject: [PATCH] Add `f_equiv/=` which performs `simpl` first.
This is similar to `f_equal/=`.
---
theories/tactics.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/tactics.v b/theories/tactics.v
index 5763d58..55d308f 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -319,6 +319,7 @@ Ltac f_equiv :=
| H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => simple apply H
end;
try simple apply reflexivity.
+Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
(* The tactic [solve_proper_unfold] unfolds the first head symbol, so that
we proceed by repeatedly using [f_equiv]. *)
--
GitLab