diff options
Diffstat (limited to 'src/Util/FixCoqMistakes.v')
-rw-r--r-- | src/Util/FixCoqMistakes.v | 10 |
1 files changed, 10 insertions, 0 deletions
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 "<infomsg>Warning: debug_intuition should not be used in production code.</infomsg>"; 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. |