diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-30 11:08:39 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-30 11:08:39 +0000 |
| commit | 3ed23b97c8d1bfbf917b540a35ee767afea28658 (patch) | |
| tree | b382d95d775b03b08a4f81b14f7517801851e139 /test-suite/success/dependentind.v | |
| parent | 10fa0c0b6b6d29901de9258d7fad402e3b6ec79a (diff) | |
Improve the dependent induction tactic to automatically find the
generalized hypotheses. Also move part of the tactic to ML and
improve the generated proof term in case of non-dependent induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11023 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/dependentind.v')
| -rw-r--r-- | test-suite/success/dependentind.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 0db172e82..482553869 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -56,7 +56,7 @@ Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ -> Proof with simpl in * ; auto ; simpl_depind. intros Γ Δ τ H. - dependent induction H generalizing Γ Δ. + dependent induction H. destruct Δ... apply weak ; apply ax. @@ -64,7 +64,7 @@ Proof with simpl in * ; auto ; simpl_depind. apply ax. destruct Δ... - specialize (IHterm Γ empty)... + specialize (IHterm Γ empty)... apply weak... apply weak... @@ -81,7 +81,7 @@ Qed. Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ. Proof with simpl in * ; simpl_depind ; auto. intros until 1. - dependent induction H generalizing Γ Δ α β. + dependent induction H. destruct Δ... apply weak ; apply ax. @@ -94,7 +94,7 @@ Proof with simpl in * ; simpl_depind ; auto. apply weak... apply abs... - specialize (IHterm Γ0 (Δ, τ))... + specialize (IHterm Γ0 α β (Δ, τ))... eapply app with τ... Save. |