diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-17 16:56:12 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-17 17:23:25 -0400 |
| commit | 4d156f212c171fe3a71f5ab403d097733c01ecf8 (patch) | |
| tree | 88d3837ef1d38ffad30d0d98fad35406437e77f4 /src/Util/FixCoqMistakes.v | |
| parent | 697505eea7a0a41086ad4775ccb7b244503940b6 (diff) | |
Work around bug #5341
Diffstat (limited to 'src/Util/FixCoqMistakes.v')
| -rw-r--r-- | src/Util/FixCoqMistakes.v | 11 |
1 files changed, 11 insertions, 0 deletions
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. |