Automatic introduction of names given before ":" in Lemma's and

Definition's is not so painless. It seems to however generally provide
"nicer" scripts so let us keep it and update the contribs and
test-suite accordingly.
Also enforced that the actual introduced names to be exactly as given
in the statements.

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

13 files changed, 33 insertions, 31 deletions

diff --git a/CHANGES b/CHANGES
index a4cd4118a..0aef24b87 100644
--- a/CHANGES
+++ b/CHANGES
@@ -106,8 +106,9 @@ Specification language
 
 - New support for local binders in the syntax of Record/Structure fields.
 - Fixpoint/CoFixpoint now support building part or all of bodies using tactics.
-- Binders given before ":" in lemmas can now be automatically
-  introduced in the context by setting option "Set Automatic Introduction".
+- Binders given before ":" in lemmas and in definitions built by tactics are
+  now automatically introduced (possible source of incompatibility that can
+  be resolved by invoking "Unset Automatic Introduction").
 
 Module system
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 840c71ec6..db60c6afc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -481,7 +481,7 @@ let prim_refiner r sigma goal =
     (* Logical rules *)
     | Intro id ->
     	if !check && mem_named_context id (named_context_of_val sign) then
-	  error "New variable is already declared";
+	  error ("Variable " ^ string_of_id id ^ " is already declared.");
         (match kind_of_term (strip_outer_cast cl) with
 	   | Prod (_,c1,b) ->
 	       let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign)
@@ -510,7 +510,7 @@ let prim_refiner r sigma goal =
 	      cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-                error "New variable is already declared";
+	      error ("Variable " ^ string_of_id id ^ " is already declared.");
 	     push_named_context_val (id,None,t) sign,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v
index 4114987d3..879a65b18 100644
--- a/test-suite/bugs/closed/shouldsucceed/1643.v
+++ b/test-suite/bugs/closed/shouldsucceed/1643.v
@@ -10,7 +10,6 @@ Definition decomp_func (s:Str) :=
 
 Theorem decomp s: s = decomp_func s.
 Proof.
-  intros s.
   case s; simpl; reflexivity.
 Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v
index 11124cddd..2d90a2f1d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1891.v
+++ b/test-suite/bugs/closed/shouldsucceed/1891.v
@@ -7,7 +7,7 @@
 
   Lemma L (x: T unit): (unit -> T unit) -> unit.
   Proof.
-    refine (fun x => match x return _ with mkT n => fun g => f (g _) end).
+    refine (match x return _ with mkT n => fun g => f (g _) end).
     trivial.
   Qed.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v
index 474ec935b..9d92fe12b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1918.v
+++ b/test-suite/bugs/closed/shouldsucceed/1918.v
@@ -66,14 +66,14 @@ Definition pEFct (F:k2) : Type :=
 Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)).
 Proof.
   red.
-  intros X Y mX mY A B f x.
+  intros A B f x.
   exact (mX (Y A)(Y B) (mY A B f) x).
 Defined.
 
 (** closure under composition *)
 Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)).
 Proof.
-  intros X Y ef1 ef2.
+  intros ef1 ef2.
   apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp.
 (* prove ext *)
   apply (e ef1).
@@ -103,7 +103,7 @@ Defined.
 (** closure under sums *)
 Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type.
 Proof.
-  intros X Y ef1 ef2.
+  intros ef1 ef2.
   set (m12:=fun (A B:Set)(f:A->B) x => match x with
     | inl y => inl _ (m ef1 f y)
     | inr y => inr _ (m ef2 f y)
@@ -144,7 +144,7 @@ Defined.
 (** closure under products *)
 Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type.
 Proof.
-  intros X Y ef1 ef2.
+  intros ef1 ef2.
   set (m12:=fun (A B:Set)(f:A->B) x => match x with
     (x1,x2) => (m ef1 f x1, m ef2 f x2) end).
   apply (mkEFct(m:=m12)); red; intros.
@@ -220,7 +220,6 @@ Defined.
 (** constants in k1 *)
 Lemma constEFct (C:Set): EFct (fun _ => C).
 Proof.
-  intro.
   set (mC:=fun A B (f:A->B)(x:C) => x).
   apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity.
 Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v
index c50ad036d..d0b3bf173 100644
--- a/test-suite/bugs/closed/shouldsucceed/2001.v
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -1,6 +1,8 @@
 (* Automatic computing of guard in "Theorem with"; check that guard is not
    computed when the user explicitly indicated it *)
 
+Unset Automatic Introduction.
+
 Inductive T : Set :=
 | v : T.
 
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index c1405cf91..b533db6ea 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -21,7 +21,6 @@ Parameter eq_img : forall (i1:img) (i2:img),
   eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2).
 
 Lemma phi_img (a:A) : img.
-  intro a.
   exists  a (phi a).
   refine ( refl_equal _).
 Defined.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 14d27924e..d4e6a82ef 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -322,7 +322,7 @@ match v in (vector _ n0) return (vector A (pred n0)) with
 end.
 
 Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
- intros A n v; case v.
+ case v.
  simpl.
  exact (Vnil A).
  simpl.
@@ -920,9 +920,7 @@ Print minus_decrease.
 
 
 
-Definition div_aux (x y:nat)(H: Acc lt x):nat.
- fix 3.
- intros.
+Fixpoint div_aux (x y:nat)(H: Acc lt x):nat.
   refine (if eq_nat_dec x 0
          then 0
          else if eq_nat_dec y 0
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 3d1c91bbe..908b5f77d 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -71,7 +71,6 @@ Record Morphism (X Y:Setoid) : Type :=
 {evalMorphism :> X -> Y}.
 
 Definition extSetoid (X Y:Setoid) : Setoid.
-intros X Y.
 constructor.
 exact (Morphism X Y).
 Defined.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 93c92b8f8..005052df2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -486,7 +486,7 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
 
 (* Jump over let-bindings. *)
 
-let compute_possible_guardness_evidences (nb,_,na) =
+let compute_possible_guardness_evidences (ids,_,na) =
   match na with
   | Some i -> [i]
   | None ->
@@ -495,7 +495,7 @@ let compute_possible_guardness_evidences (nb,_,na) =
 	 but doing it properly involves delta-reduction, and it finally
          doesn't seem to worth the effort (except for huge mutual
 	 fixpoints ?) *)
-      interval 0 (nb - 1)
+      interval 0 (List.length ids - 1)
 
 type recursive_preentry =
   identifier list * constr option list * types list
@@ -527,7 +527,7 @@ let interp_recursive isfix fixl notations =
   let evd = consider_remaining_unif_problems env_rec !evdref in
   let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
   let fixtypes = List.map (nf_evar evd) fixtypes in
-  let fixctxlength = List.map (fun (_,ctx) -> rel_context_nhyps ctx) fixctxs in
+  let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
   let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
   List.iter (Option.iter (check_evars env_rec Evd.empty evd)) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
@@ -537,7 +537,7 @@ let interp_recursive isfix fixl notations =
   end;
 
   (* Build the fix declaration block *)
-  (fixnames,fixdefs,fixtypes), list_combine3 fixctxlength fiximps fixannots
+  (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
 
 let interp_fixpoint = interp_recursive true
 let interp_cofixpoint = interp_recursive false
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 57c8e0198..3a6bb18c1 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -118,20 +118,22 @@ type recursive_preentry =
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * (int * manual_implicits * int option) list
+    recursive_preentry * (name list * manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
-    recursive_preentry * (int * manual_implicits * int option) list
+    recursive_preentry * (name list * manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  bool -> recursive_preentry * (int * manual_implicits * int option) list -> 
+  bool ->
+  recursive_preentry * (name list * manual_implicits * int option) list -> 
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
-  bool -> recursive_preentry * (int * manual_implicits * int option) list ->
+  bool ->
+  recursive_preentry * (name list * manual_implicits * int option) list ->
     decl_notation list -> unit
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 5e99e9a9e..01cfd22e8 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -274,7 +274,10 @@ let rec_tac_initializer finite guard thms snl =
        | _ -> assert false
 
 let start_proof_with_initialization kind recguard thms snl hook =
-  let intro_tac (_, (_, (len, _))) = Refiner.tclDO len Tactics.intro in
+  let intro_tac (_, (_, (ids, _))) =
+    Refiner.tclMAP (function
+    | Name id -> Tactics.intro_mustbe_force id
+    | Anonymous -> Tactics.intro) (List.rev ids) in
   let init_tac,guard = match recguard with
   | Some (finite,guard,init_tac) ->
       let rec_tac = rec_tac_initializer finite guard thms snl in
@@ -295,7 +298,7 @@ let start_proof_with_initialization kind recguard thms snl hook =
       (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
   match thms with
   | [] -> anomaly "No proof to start"
-  | (id,(t,(len,imps)))::other_thms ->
+  | (id,(t,(_,imps)))::other_thms ->
       let hook strength ref =
         let other_thms_data =
           if other_thms = [] then [] else
@@ -315,10 +318,10 @@ let start_proof_com kind thms hook =
     let (env, ctx), imps = interp_context_evars evdref env0 bl in
     let t', imps' = interp_type_evars_impls ~evdref env t in
     Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
-    let len = List.length ctx in
+    let ids = List.map pi1 ctx in
       (compute_proof_name (fst kind) sopt,
       (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx),
-       (len, imps @ lift_implicits len imps'),
+       (ids, imps @ lift_implicits (List.length ids) imps'),
        guard)))
     thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index b75d56999..40a1d802c 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -28,8 +28,8 @@ val start_proof_com : goal_kind ->
 
 val start_proof_with_initialization : 
   goal_kind -> (bool * lemma_possible_guards * tactic list option) option ->
-  (identifier * (types * (int * Impargs.manual_explicitation list))) list ->
-  int list option -> declaration_hook -> unit
+  (identifier * (types * (name list * Impargs.manual_explicitation list))) list
+  -> int list option -> declaration_hook -> unit
 
 (** A hook the next three functions pass to cook_proof *)
 val set_save_hook : (Proof.proof -> unit) -> unit