A bit of cleaning around name generation + creation of dedicated file namegen.ml

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

11 files changed, 28 insertions, 34 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 5de89baa6..3ba6b9f1b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,6 +12,7 @@ open Pp
 open Util
 open Names
 open Nameops
+open Namegen
 open Term
 open Termops
 open Inductiveops
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index bfb5039d5..2b583af40 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -223,7 +223,7 @@ let rec deanonymize ids =
   function
       PatVar (loc,Anonymous) ->
 	let (found,known) = !ids in
-	let new_id=Nameops.next_ident_away dummy_prefix known in
+	let new_id=Namegen.next_ident_away dummy_prefix known in
 	let _= ids:= (loc,new_id) :: found , new_id :: known in
 	  PatVar (loc,Name new_id)
     | PatVar (loc,Name id) as pat ->
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index bde403657..8c47497a1 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -28,6 +28,7 @@ open Tactics
 open Tacticals
 open Term
 open Termops
+open Namegen
 open Reductionops
 open Goptions
 
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index d535e56e1..0d1699b1c 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -18,7 +18,7 @@
 
 open Util
 open Names
-open Nameops
+open Namegen
 open Term
 open Declarations
 open Tactics
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index a9ced0a69..0553a1498 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -53,6 +53,7 @@ open Declarations
 open Environ
 open Inductive
 open Termops
+open Namegen
 open Inductiveops
 open Ind_tables
 open Indrec
@@ -60,7 +61,7 @@ open Indrec
 let hid = id_of_string "H"
 let xid = id_of_string "X"
 let default_id_of_sort = function InProp _ | InSet -> hid | InType _ -> xid
-let fresh env id = next_global_ident_away false id []
+let fresh env id = next_global_ident_away id []
 
 let build_dependent_inductive ind (mib,mip) =
   let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7db751372..f5e1fc5c4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -15,6 +15,7 @@ open Nameops
 open Univ
 open Term
 open Termops
+open Namegen
 open Inductive
 open Inductiveops
 open Environ
diff --git a/tactics/inv.ml b/tactics/inv.ml
index eb978ba48..46ca8161c 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Namegen
 open Global
 open Sign
 open Environ
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index c2be67d75..d0f6e8226 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Namegen
 open Sign
 open Evd
 open Printer
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 23611b657..67a73b9be 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -53,6 +53,7 @@ open Util
 open Names
 open Term
 open Termops
+open Namegen
 open Tacmach
 open Sign
 open Environ
@@ -131,7 +132,7 @@ let replace_in_array keep_length env sigma a =
 
 let fresh env n =
   let id = match n with Name x -> x | _ -> id_of_string "_H" in
-  next_global_ident_away true id (ids_of_named_context (named_context env))
+  next_ident_away_in_goal id (ids_of_named_context (named_context env))
 
 let rec compute_metamap env sigma c = match kind_of_term c with
   (* le terme est directement une preuve *)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index cd2a14236..d3d488183 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -15,6 +15,7 @@ open Pp
 open Util
 open Names
 open Nameops
+open Namegen
 open Term
 open Termops
 open Sign
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 368502d40..48e45e8d8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -15,6 +15,7 @@ open Nameops
 open Sign
 open Term
 open Termops
+open Namegen
 open Declarations
 open Inductive
 open Inductiveops
@@ -175,11 +176,8 @@ let rename_hyp      = Tacmach.rename_hyp
 (*          Fresh names                                       *)
 (**************************************************************)
 
-let fresh_id_avoid avoid id =
-  next_global_ident_away true id avoid
-
 let fresh_id avoid id gl =
-  fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id
+  next_ident_away_in_goal id (avoid@(pf_ids_of_hyps gl))
 
 (**************************************************************)
 (*          Fixpoints and CoFixpoints                         *)
@@ -529,7 +527,7 @@ let intro_move idopt hto = match idopt with
 
 let pf_lookup_hypothesis_as_renamed env ccl = function
   | AnonHyp n -> pf_lookup_index_as_renamed env ccl n
-  | NamedHyp id -> pf_lookup_name_as_renamed env ccl id
+  | NamedHyp id -> pf_lookup_name_as_displayed env ccl id
 
 let pf_lookup_hypothesis_as_renamed_gen red h gl =
   let env = pf_env gl in
@@ -2446,7 +2444,7 @@ let specialize_hypothesis id gl =
       
 
 let specialize_hypothesis id gl =
-  if occur_id [] id (pf_concl gl) then
+  if occur_var (pf_env gl) id (pf_concl gl) then
     tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl 
   else specialize_hypothesis id gl
 
@@ -3442,7 +3440,7 @@ let interpretable_as_section_decl d1 d2 = match d1,d2 with
   | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2
   | (_,None,t1), (_,_,t2) -> eq_constr t1 t2
 
-let abstract_subproof name tac gl =
+let abstract_subproof id tac gl =
   let current_sign = Global.named_context()
   and global_sign = pf_hyps gl in
   let sign,secsign =
@@ -3453,29 +3451,17 @@ let abstract_subproof name tac gl =
         then (s1,push_named_context_val d s2)
 	else (add_named_decl d s1,s2))
       global_sign (empty_named_context,empty_named_context_val) in
-  let na = next_global_ident_away false name (pf_ids_of_hyps gl) in
+  let id = next_global_ident_away id (pf_ids_of_hyps gl) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
-    if occur_existential concl then
-      error "\"abstract\" cannot handle existentials.";
-    let lemme =
-      start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
-      let _,(const,_,kind,_) =
-	try
-	  by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac));
-	  let r = cook_proof ignore in
-	    delete_current_proof (); r
-	with
-	    e ->
-	      (delete_current_proof(); raise e)
-      in   (* Faudrait un peu fonctionnaliser cela *)
-      let cd = Entries.DefinitionEntry const in
-      let con = Declare.declare_internal_constant na (cd,IsProof Lemma) in
-	constr_of_global (ConstRef con)
-    in
-      exact_no_check
-	(applist (lemme,
-		 List.rev (Array.to_list (instance_from_named_context sign))))
-	gl
+  if occur_existential concl then
+    error "\"abstract\" cannot handle existentials.";
+  let const = Pfedit.build_constant_by_tactic secsign concl
+    (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in
+  let cd = Entries.DefinitionEntry const in
+  let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in
+  exact_no_check
+    (applist (lem,List.rev (Array.to_list (instance_from_named_context sign))))
+    gl
 
 let tclABSTRACT name_op tac gl =
   let s = match name_op with
@@ -3497,7 +3483,7 @@ let admit_as_an_axiom gl =
 	 else (add_named_decl d s1,s2))
       global_sign (empty_named_context,empty_named_context) in
   let name = add_suffix (get_current_proof_name ()) "_admitted" in
-  let na = next_global_ident_away false name (pf_ids_of_hyps gl) in
+  let na = next_global_ident_away name (pf_ids_of_hyps gl) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
   if occur_existential concl then error"\"admit\" cannot handle existentials.";
   let axiom =