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

4 files changed, 11 insertions, 9 deletions

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 96bda6ecc..2db253373 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -16,6 +16,7 @@ open Sign
 open Evd
 open Term
 open Termops
+open Namegen
 open Reductionops
 open Environ
 open Type_errors
@@ -71,7 +72,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
           user_err_loc (loc,"start_proof",pr_id id ++ str " already exists");
         id
     | None ->
-	next_global_ident_away false (id_of_string "Unnamed_thm")
+	next_global_ident_away (id_of_string "Unnamed_thm")
  	  (Pfedit.get_all_proof_names ())
   in
   let evm, c, typ, imps =
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 4eb05df74..bc4d834d4 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -15,6 +15,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Namegen
 open Declarations
 open Inductiveops
 open Environ
@@ -1501,7 +1502,7 @@ let make_prime_id name =
 
 let prime avoid name =
   let previd, id = make_prime_id name in
-    previd, next_ident_away_from id avoid
+    previd, next_ident_away id avoid
 
 let make_prime avoid prevname =
   let previd, id = prime !avoid prevname in
@@ -1510,7 +1511,7 @@ let make_prime avoid prevname =
 
 let eq_id avoid id =
   let hid = id_of_string ("Heq_" ^ string_of_id id) in
-  let hid' = next_ident_away_from hid avoid in
+  let hid' = next_ident_away hid avoid in
     hid'
 
 let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
@@ -1588,7 +1589,7 @@ let constr_of_pat env isevars arsign pat avoid =
 (* shadows functional version *)
 let eq_id avoid id =
   let hid = id_of_string ("Heq_" ^ string_of_id id) in
-  let hid' = next_ident_away_from hid !avoid in
+  let hid' = next_ident_away hid !avoid in
     avoid := hid' :: !avoid;
     hid'
 
@@ -1784,7 +1785,7 @@ let abstract_tomatch env tomatchs tycon =
 	   | _ ->
 	       let tycon = Option.map
 		 (fun t -> subst_term_occ all_occurrences (lift 1 c) (lift 1 t)) tycon in
-	       let name = next_ident_away_from (id_of_string "filtered_var") names in
+	       let name = next_ident_away (id_of_string "filtered_var") names in
 		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
 	       (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
 	       name :: names, tycon)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 26ac445c3..b96c58755 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -47,7 +47,7 @@ let interp_typeclass_context_evars isevars env avoid l =
     (fun (env, ids, params) (iid, bk, cl) ->
       let t' = interp_binder_evars isevars env (snd iid) cl in
       let i = match snd iid with
-	| Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids
+	| Anonymous -> Namegen.next_name_away (Namegen.named_hd env t' Anonymous) ids
 	| Name id -> id
       in
       let d = (i,None,t') in
@@ -58,7 +58,7 @@ let interp_constrs_evars isevars env avoid l =
   List.fold_left
     (fun (env, ids, params) t ->
       let t' = interp_binder_evars isevars env Anonymous t in
-      let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in
+      let id = Namegen.next_name_away (Namegen.named_hd env t' Anonymous) ids in
       let d = (id,None,t') in
 	(push_named d env, id :: ids, d::params))
     (env, avoid, []) l
@@ -129,7 +129,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	  id
     | Anonymous ->
 	let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
-	  Termops.next_global_ident_away false i (Termops.ids_of_context env)
+	  Namegen.next_global_ident_away i (Termops.ids_of_context env)
   in
   let env' = push_rel_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 4dd3dd32b..8cf28a0dd 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -166,7 +166,7 @@ module Coercion = struct
 		 | Type x, Type y when x = y -> None (* false *)
 		 | _ -> subco ())
 	  | Prod (name, a, b), Prod (name', a', b') ->
-	      let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
+	      let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
 	      let env' = push_rel (name', None, a') env in
 	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 		(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)