Diff to get outrageous to work with Coq 8.4pl4 (output of svn diff)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Index: Context.v | |
=================================================================== | |
--- Context.v (revision 16) | |
+++ Context.v (working copy) | |
@@ -157,7 +157,7 @@ | |
change (PopCtx T' (AtCtx G n) T2) in a2. | |
destruct a2 as (T2,a2). | |
- exact (tr (fun xa=>_ = exAtCtx (popCtx (xa_a xa) T')) (IHa1 _ a2) (eq_refl _)). | |
+ exact (tr (fun xa=>exAtCtx (popCtx a1 T') = exAtCtx (popCtx (xa_a xa) T')) (IHa1 _ a2) (eq_refl _)). | |
Defined. | |
Implicit Arguments atCtxUniq [G n T1 T2]. | |
Index: TreeSyntax.v | |
=================================================================== | |
--- TreeSyntax.v (revision 16) | |
+++ TreeSyntax.v (working copy) | |
@@ -478,7 +478,7 @@ | |
replace n0 with (length (firstn n G));subst n0. | |
apply tfGoodBump_O with (1 := H0). | |
rewrite firstn_length. | |
- apply MinMax.min_l with (1 := H). | |
+ apply min_l with (1 := H). | |
Qed. | |
Lemma tfGoodSubstNest GL GR F b : (b < length GL)->let X := fBump (S b) O (nth b GL Uv) in |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment