Diff to get outrageous to work with Coq trunk (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: TreeItrp.v | |
=================================================================== | |
--- TreeItrp.v (revision 16) | |
+++ TreeItrp.v (working copy) | |
@@ -1,3 +1,4 @@ | |
+Set Asymmetric Patterns. | |
Require Import List. | |
Require Import Utils. | |
Index: Context.v | |
=================================================================== | |
--- Context.v (revision 16) | |
+++ Context.v (working copy) | |
@@ -1,3 +1,4 @@ | |
+Set Asymmetric Patterns. | |
Require Import Utils. | |
Require Import SimpSubst. | |
@@ -121,7 +122,7 @@ | |
: forall G (s:CtxS G) n T (a:AtCtx (ctx s) n T),P _ _ _ a. | |
refine (fix atCtxIndS G s n := match s in CtxS G return forall T (a:AtCtx (ctx s) n T),P _ _ _ a with | |
empCtxS => _ | | |
- extCtxS _ s _ => _ | |
+ extCtxS G0 s0 _ => _ | |
end);clear G s;simpl;intro. | |
intro. | |
@@ -157,7 +158,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]. | |
@@ -222,8 +223,8 @@ | |
Definition extSCtxInv GL n G T (xg:ExtCtx GL (S n) (extCtx G T)) (P:forall n G T,ExtCtx GL n (extCtx G T)->Type) | |
(xgS:forall xg:ExtCtx GL n G,P _ _ _ (extSCtx xg T)) | |
: P _ _ _ xg. | |
- pose (P' n Gx (xg:ExtCtx GL n Gx) := forall ne:IsExtCtx Gx, | |
- P _ _ _ (tr (ExtCtx GL n) (extCtxUnfold ne) xg)). | |
+ pose (P' n0 Gx (xg:ExtCtx GL n0 Gx) := forall ne:IsExtCtx Gx, | |
+ P _ _ _ (tr (ExtCtx GL n0) (extCtxUnfold ne) xg)). | |
assert (Peq := match G as G return forall T xg,P (S n) G T xg = P _ (ctx (ctxSc G)) _ xg | |
with ctx _ _ => fun _ _=>eq_refl _ end T). | |
apply (tr (fun C=>C) (eq_sym (Peq _))). | |
@@ -233,7 +234,7 @@ | |
extSCtx _ _ xg0 _ => fun Hn HG=>_ | |
end (eq_refl _) (eq_refl _)). | |
revert xg0. | |
- apply (tr (fun _=>_) (eq_sym (Sinj Hn))). | |
+ apply Sinj in Hn; subst. | |
apply (tr (fun GT=>forall xg,P' _ _ (extSCtx xg (projT2 GT))) (extCtxInj HG)). | |
simpl. | |
intros ? ?. | |
@@ -379,7 +380,9 @@ | |
change (elBump P (extSCtx xg T') (ctxProj (popCtx a T')) = | |
ctxProj (popCtx (atBumpLo P xg a Ho) (elBump P xg T'))). | |
apply (tr (fun X=>_ = X) (ctxProj_pop (atBumpLo P xg a Ho) (elBump P xg T'))). | |
- apply (tr (fun X=>_ = fun g=>X (projT1 g)) (IHa _ Ho xg)). | |
+ specialize (IHa _ Ho xg). | |
+ let XT := match type of IHa with _ = _ :> ?XT => constr:(XT) end in | |
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) IHa). | |
reflexivity. | |
Defined. | |
Implicit Arguments ctxProj_BumpLo [GL l G n T]. | |
@@ -407,7 +410,9 @@ | |
ctxProj (popCtx (atBumpHi P xg a Ho) (elBump P xg T'))). | |
apply (tr (fun X=>elBump P (extSCtx xg T') X = _) (ctxProj_pop a T')). | |
apply (tr (fun X=>_ = X) (ctxProj_pop (atBumpHi P xg a Ho) (elBump P xg T'))). | |
- apply (tr (fun X=>_ = fun g=>X (projT1 g)) (IHxg _ Ho _ a)). | |
+ specialize (IHxg _ Ho _ a). | |
+ let XT := match type of IHxg with _ = _ :> ?XT => constr:(XT) end in | |
+ apply (tr (fun X:XT=>_ = fun g=>X (projT1 g)) IHxg). | |
reflexivity. | |
Defined. | |
Implicit Arguments ctxProj_BumpHi [GL l G n T]. | |
@@ -519,7 +524,9 @@ | |
change (PopCtx T (AtCtx G a) P') in a'. | |
destruct a' as (P',a'). | |
- apply (tr (fun _=>_) (IHxg _ a')). | |
+ specialize (IHxg _ a'). | |
+ let XT := match type of IHxg with _ = _ :> ?XT => constr:(XT) end in | |
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) IHxg). | |
reflexivity. | |
Defined. | |
Implicit Arguments atMBumpTEq [GL a b P G P']. | |
@@ -576,7 +583,9 @@ | |
change (elSubst (extSCtx xg T') (ctxProj (popCtx a T')) p = | |
ctxProj (popCtx (atSubstLt xg a Ho p) (elSubst xg T' p))). | |
apply (tr (fun X=>_ = X) (ctxProj_pop (atSubstLt xg a Ho p) (elSubst xg T' p))). | |
- apply (tr (fun X=>_ = fun g=>X (projT1 g)) (IHa _ Ho xg)). | |
+ specialize (IHa _ Ho xg). | |
+ let XT := match type of IHa with _ = _ :> ?XT => constr:(XT) end in | |
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) IHa). | |
reflexivity. | |
Defined. | |
Implicit Arguments ctxProj_SubstLt [GL P l G n T]. | |
@@ -605,8 +614,10 @@ | |
ctxProj (popCtx (atSubstGt xg a Ho p) (elSubst xg T' p))). | |
apply (tr (fun X=>elSubst (extSCtx xg T') X p = _) (ctxProj_pop a T')). | |
apply (tr (fun X=>_ = X) (ctxProj_pop (atSubstGt xg a Ho p) (elSubst xg T' p))). | |
- apply (tr (fun X=>_ = fun g=>X (projT1 g)) (IHxg _ Ho _ a)). | |
- reflexivity. | |
+ specialize (IHxg _ Ho _ a). | |
+ let XT := match type of IHxg with _ = _ :> ?XT => constr:(XT) end in | |
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) IHxg). | |
+ reflexivity. | |
Defined. | |
Implicit Arguments ctxProj_SubstGt [GL P l G n T]. | |
@@ -637,7 +648,8 @@ | |
simpl ctxTp. | |
intros ? ? a' ? ?. | |
simpl elMBump. | |
- apply (tr (fun t=>_ = fun g=>t (projT1 g)) H). | |
+ let XT := match type of H with _ = _ :> ?XT => constr:(XT) end in | |
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) H). | |
simpl atMBumpTEq. | |
refine (match atMBumpTEq b' xg a' as teq | |
return ctxProj (tr (AtCtx (extCtx (ctx s) _) _) (tr _ teq _) _) = | |
@@ -661,7 +673,8 @@ | |
intros. | |
change ((fun g:ctxSubst (extSCtx xg T) p=>elSubst xg (ctxProj a) p (projT1 g)) = | |
(fun g=>elSubst xg (elMBump xg a p) p (projT1 g))). | |
- apply (tr (fun X=>_ = fun g:ctxSubst (extSCtx xg T) p=>X (projT1 g)) H). | |
+ let XT := match type of H with _ = _ :> ?XT => constr:(XT) end in | |
+ apply (tr (fun X : XT=>_ = fun g=>X (projT1 g)) H). | |
reflexivity. | |
Defined. | |
Implicit Arguments ctxProj_SubstEq [GL P n G P']. | |
Index: TreeSyntax.v | |
=================================================================== | |
--- TreeSyntax.v (revision 16) | |
+++ TreeSyntax.v (working copy) | |
@@ -1,3 +1,4 @@ | |
+Set Asymmetric Patterns. | |
Require Import List. | |
Require Import Compare_dec. | |
@@ -478,7 +479,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 | |
@@ -872,8 +873,8 @@ | |
apply ctxProjGood with (1 := H0). | |
simpl in H3. | |
rewrite <- H2. | |
- exact H3. | |
+ assumption. | |
refine (let H := IHSimpFamOK _ in _). | |
apply tcGoodCons with (1 := H1) (2 := H0). | |
- apply tfGoodPi with (1 := H1) (2 := H2). | |
+ apply tfGoodPi; assumption. | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment