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

4 files changed, 19 insertions, 14 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 93c92b8f85..005052df26 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 57c8e0198b..3a6bb18c16 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 5e99e9a9eb..01cfd22e81 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 b75d569999..40a1d802cb 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