From 2deb16b97b4558d92e2a431b49f1168a9281732c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 10:57:37 -0700 Subject: Transparent version of f_equal2 --- src/Util/FixCoqMistakes.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util/FixCoqMistakes.v') diff --git a/src/Util/FixCoqMistakes.v b/src/Util/FixCoqMistakes.v index 129344f83..28f1ac757 100644 --- a/src/Util/FixCoqMistakes.v +++ b/src/Util/FixCoqMistakes.v @@ -12,3 +12,13 @@ Tactic Notation "intuition" := intuition auto. (** A version of [intuition] that allows you to see how the old [intuition] tactic solves the proof. *) Ltac debug_intuition := idtac "Warning: debug_intuition should not be used in production code."; intuition debug auto with *. + +(** [Coq.Init.Logic.f_equal2] is opaque. A transparent version would serve us better. *) +Definition f_equal2 {A1 A2 B} (f : A1 -> A2 -> B) {x1 y1 : A1} {x2 y2 : A2} (H : x1 = y1) + := match H in (_ = y) return (x2 = y2 -> f x1 x2 = f y y2) with + | eq_refl => + fun H0 : x2 = y2 => + match H0 in (_ = y) return (f x1 x2 = f x1 y) with + | eq_refl => eq_refl + end + end. -- cgit v1.2.3