From 4d156f212c171fe3a71f5ab403d097733c01ecf8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 17 Oct 2017 16:56:12 -0400 Subject: Work around bug #5341 --- src/Util/FixCoqMistakes.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/Util/FixCoqMistakes.v') diff --git a/src/Util/FixCoqMistakes.v b/src/Util/FixCoqMistakes.v index 26fc103c1..c59b92a74 100644 --- a/src/Util/FixCoqMistakes.v +++ b/src/Util/FixCoqMistakes.v @@ -27,3 +27,14 @@ Definition f_equal2 {A1 A2 B} (f : A1 -> A2 -> B) {x1 y1 : A1} {x2 y2 : A2} (H : | eq_refl => eq_refl end end. + +(** Work around BZ#5341, https://coq.inria.fr/bugs/show_bug.cgi?id=5341, [subst] fails with bogus error message about universe polymorphism *) +Local Theorem create_internal_eq_rew_r_dep : forall A (a : A) (x : A) (e : a = x), + e = e -> True. +Proof. + intros ? ? ? H. + match goal with |- ?G => assert G end; + [ rewrite -> H + | rewrite <- H ]; + constructor. +Defined. -- cgit v1.2.3