From 3ed23b97c8d1bfbf917b540a35ee767afea28658 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 30 May 2008 11:08:39 +0000
Subject: 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
---
 test-suite/success/dependentind.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 0db172e82a..4825538691 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.
-- 
cgit v1.2.3