From 29a0e002bf4a8d7530a05ac3d49debaf138fb183 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 21 Apr 2018 15:03:19 +0200
Subject: [PATCH] f_equiv: recognize 2-level pointwise_relation
---
theories/tactics.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/tactics.v b/theories/tactics.v
index 4b42a8f6..eb0b3969 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -316,6 +316,7 @@ Ltac f_equiv :=
query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *)
| H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => simple apply H
+ | H : pointwise_relation _ (pointwise_relation _ ?R) ?f ?g |- ?R (?f ?x ?y) (?g ?x ?y) => simple apply H
end;
try simple apply reflexivity.
Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
--
GitLab