Fixes in dependent induction tactic, putting things in better order for

simplifications (homogeneous equations first).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11398 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 27 insertions, 19 deletions

diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 4825538691..48b07db83d 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,10 +1,10 @@
 Require Import Coq.Program.Program.
-Set Implicit Arguments.
-Unset Strict Implicit.
+Set Manual Implicit Arguments.
+
 
 Variable A : Set.
 
-Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall n, vector n -> vector (S n).
+Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n).
 
 Goal forall n, forall v : vector (S n), vector n.
 Proof.
@@ -35,24 +35,32 @@ Inductive ctx : Type :=
 | empty : ctx
 | snoc : ctx -> type -> ctx.
 
-Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity).
+Bind Scope context_scope with ctx.
+Delimit Scope context_scope with ctx.
+
+Arguments Scope snoc [context_scope].
+
+Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity) : context_scope.
 
-Fixpoint conc (Γ Δ : ctx) : ctx :=
+Fixpoint conc (Δ Γ : ctx) : ctx :=
   match Δ with
     | empty => Γ
-    | snoc Δ' x => snoc (conc Γ Δ') x
+    | snoc Δ' x => snoc (conc Δ' Γ) x
   end.
 
-Notation " Γ ; Δ " := (conc Γ Δ) (at level 25, left associativity).
+Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope.
 
 Inductive term : ctx -> type -> Type :=
-| ax : forall Γ τ, term (Γ, τ) τ
-| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ, τ') τ
-| abs : forall Γ τ τ', term (Γ , τ) τ' -> term Γ (τ --> τ')
+| ax : forall Γ τ, term (snoc Γ τ) τ
+| weak : forall Γ τ, term Γ τ -> forall τ', term (snoc Γ τ') τ
+| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ')
 | app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'.
 
-Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ -> 
-  forall τ', term (Γ , τ' ; Δ) τ.
+Notation " Γ |- τ " := (term Γ τ) (at level 0).
+
+
+Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> 
+  forall τ', term (Γ , τ' ;; Δ) τ.
 Proof with simpl in * ; auto ; simpl_depind.
   intros Γ Δ τ H.
 
@@ -64,21 +72,21 @@ Proof with simpl in * ; auto ; simpl_depind.
     apply ax.
     
   destruct Δ...
-    specialize (IHterm Γ empty)... 
-    apply weak...
+    specialize (IHterm empty Γ)... 
+    apply weak... 
 
     apply weak...
 
   destruct Δ...
-    apply weak ; apply abs ; apply H.
+    apply weak. apply abs ; apply H.
 
     apply abs...
-    specialize (IHterm Γ0 (Δ, t, τ))...
+    specialize (IHterm (Δ, t, τ)%ctx Γ0)...
 
   apply app with τ...
 Qed.
 
-Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
+Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ;; Δ) τ -> term (Γ, β, α ;; Δ) τ.
 Proof with simpl in * ; simpl_depind ; auto.
   intros until 1.
   dependent induction H.
@@ -89,12 +97,12 @@ Proof with simpl in * ; simpl_depind ; auto.
     apply ax.
 
   destruct Δ...
-    pose (weakening (Γ:=Γ0) (Δ:=(empty, α)))...
+    pose (weakening Γ0 (empty, α))...
 
     apply weak...
 
   apply abs...
-  specialize (IHterm Γ0 α β (Δ, τ))...
+  specialize (IHterm (Δ, τ)%ctx Γ0 α β)...
 
   eapply app with τ...
 Save.