Skip to content

Instantly share code, notes, and snippets.

@JasonGross
Created August 19, 2014 19:16
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save JasonGross/e8125ba420b5b2be6662 to your computer and use it in GitHub Desktop.
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