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

6 files changed, 21 insertions, 15 deletions

diff --git a/library/nameops.ml b/library/nameops.ml
index 6c5000dfef..563fa02102 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -143,6 +143,8 @@ let name_fold f na a =
   | Name id -> f id a
   | Anonymous -> a
 
+let name_iter f na = name_fold (fun x () -> f x) na ()
+
 let name_cons na l =
   match na with
   | Anonymous -> l 
diff --git a/library/nameops.mli b/library/nameops.mli
index 336099a2ff..10dfecc484 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -34,6 +34,7 @@ val next_name_away_with_default :
 val out_name : name -> identifier
 
 val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a
+val name_iter : (identifier -> unit) -> name -> unit
 val name_cons : name -> identifier list -> identifier list
 val name_app : (identifier -> identifier) -> name -> name
 val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * name
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index ba53d127e9..d4b21fba50 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -221,12 +221,15 @@ let rec pat_of_raw metas vars = function
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
   | RLambda (_,na,bk,c1,c2) ->
+      name_iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | RProd (_,na,bk,c1,c2) ->
+  | RProd (_,na,bk,c1,c2) -> 
+      name_iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
   | RLetIn (_,na,c1,c2) ->
+      name_iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
   | RSort (_,s) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fa0dd6e0c4..9940f04b5a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2173,8 +2173,8 @@ let abstract_args gl id =
 	  let liftargty = lift (List.length ctx) argty in
 	  let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
 	    match kind_of_term arg with
-	    | Var _ | Rel _ | Ind _ when convertible -> 
-		(subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env)
+(* 	    | Var _ | Rel _ | Ind _ when convertible ->  *)
+(* 		(subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env) *)
 	    | _ ->
 		let name = get_id name in
 		let decl = (Name name, None, ty) in
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.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index be2f176d37..6c4fe71fcd 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -384,6 +384,7 @@ Ltac simplify_one_dep_elim_term c :=
       intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ;
         case hyp ; clear hyp
     | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
+    | forall x, _ => intro x || (let H := fresh x in rename x into H ; intro x) (* Try to keep original names *)
     | _ => intro
   end.
 
@@ -479,9 +480,11 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
-Ltac introduce p := 
-  first [ match p with _ => idtac end (* Already there *)
-    | intros until p | intros ].
+Ltac introduce p := first [ 
+  match p with _ => (* Already there, generalize dependent hyps *) 
+    generalize dependent p ; intros p 
+  end
+  | intros until p | intros ].
 
 Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
 Ltac do_ind p := introduce p ; (induction p || elim_ind p).