diff options
| author | msozeau | 2009-04-10 19:23:58 +0000 |
|---|---|---|
| committer | msozeau | 2009-04-10 19:23:58 +0000 |
| commit | e2655d38d11b072da0e5f4d40b05adbea73c8b8d (patch) | |
| tree | 7fa52c241089222050a84d2b47576e58d6e8492e /test-suite | |
| parent | 4cc6bd53bca5441c9960ba55818b5ddfa8c8d13b (diff) | |
Fix premature optimisation in dependent induction: even variable args need
to be generalized as they may appear in other arguments or their types.
Try to keep the original names around as well, using the ones found in
the goal. This only requires that interning a pattern [forall x, _]
properly declares [x] as a metavariable, binding instances are already
part of the substitutions computed by [extended_matches].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/dependentind.v | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 3ab7682d9e..f0b700adb9 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -1,7 +1,6 @@ Require Import Coq.Program.Program. Set Manual Implicit Arguments. - Variable A : Set. Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n). @@ -73,22 +72,20 @@ Proof with simpl in * ; eqns ; eauto with lambda. dependent induction H. - destruct Δ as [|Δ τ']... + destruct Δ as [|Δ τ'']... destruct Δ as [|Δ τ'']... destruct Δ as [|Δ τ'']... apply abs. - - specialize (IHterm (Δ, τ'', τ) Γ0)... + specialize (IHterm (Δ, τ'', τ0) Γ)... intro. eapply app... -Qed. +Defined. Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. Proof with simpl in * ; eqns ; eauto. intros until 1. - dependent induction H. destruct Δ ; eqns. @@ -97,12 +94,12 @@ Proof with simpl in * ; eqns ; eauto. apply ax. destruct Δ... - pose (weakening Γ0 (empty, α))... + pose (weakening Γ (empty, α))... apply weak... apply abs... - specialize (IHterm (Δ, τ))... + specialize (IHterm (Δ, τ0))... eapply app... Defined. @@ -129,5 +126,5 @@ Inductive Ev : forall t, Exp t -> Exp t -> Prop := Ev (Fst e) e1. Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2). -intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption. +intros t1 t2 e e1 ev. dependent destruction ev. exists e3 ; assumption. Qed. |