Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Diff to get outrageous to work with Coq 8.4pl4 (output of svn diff)
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
You can’t perform that action at this time.