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

19 files changed, 92 insertions, 85 deletions

diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 6365043611..46e5b50aa8 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -22,6 +22,7 @@ open Tacticals
 open Fol
 open Names
 open Nameops
+open Namegen
 open Termops
 open Coqlib
 open Hipattern
@@ -125,7 +126,7 @@ let rename_global r =
   with Not_found ->
     let rec loop id =
       if Hashtbl.mem used_names id then
-	loop (lift_ident id)
+	loop (lift_subscript id)
       else begin
 	Hashtbl.add used_names id ();
 	let s = string_of_id id in
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 47381f6d80..73b51cfe7d 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -13,6 +13,7 @@ open Util
 open Names
 open Term
 open Declarations
+open Namegen
 open Nameops
 open Libnames
 open Table
@@ -92,7 +93,7 @@ type env = identifier list * Idset.t
 (*s Generic renaming issues for local variable names. *)
 
 let rec rename_id id avoid =
-  if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
+  if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
 
 let rec rename_vars avoid = function
   | [] ->
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index d119dbe8ec..71bb634dad 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -20,7 +20,7 @@ open Inductive
 open Termops
 open Inductiveops
 open Recordops
-open Nameops
+open Namegen
 open Summary
 open Libnames
 open Nametab
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 043bf0fe75..df9f02dfd6 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -12,6 +12,7 @@ open Names
 open Term
 open Declarations
 open Nameops
+open Namegen
 open Summary
 open Libobject
 open Goptions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3d789b92ed..e8ec962b44 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -2,6 +2,7 @@ open Printer
 open Util
 open Term
 open Termops
+open Namegen
 open Names
 open Declarations
 open Pp
@@ -1358,7 +1359,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
     | None -> anomaly "No tcc proof !!"
     | Some lemma ->
 	fun gls ->
-(* 	  let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in *)
+(* 	  let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
 (* 	  let ids = hid::pf_ids_of_hyps gls in  *)
 	  tclTHENSEQ
 	    [
@@ -1581,7 +1582,7 @@ let prove_principle_for_gen
   let start_tac gls =
     let hyps = pf_ids_of_hyps gls in
       let hid =
-	next_global_ident_away true
+	next_ident_away_in_goal
 	  (id_of_string "prov")
 	  hyps
       in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index ff4d1e972f..b756492b51 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -2,6 +2,7 @@ open Printer
 open Util
 open Term
 open Termops
+open Namegen
 open Names
 open Declarations
 open Pp
@@ -67,7 +68,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     match predicates with
     | [] -> []
     |(Name x,v,t)::predicates ->
-       let id =  Nameops.next_ident_away x avoid in
+       let id =  Namegen.next_ident_away x avoid in
        Hashtbl.add tbl id x;
        (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
     | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder "
@@ -330,7 +331,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
      observe (str "new_principle_type : " ++ pr_lconstr new_principle_type);
   let new_princ_name =
-    next_global_ident_away true (id_of_string "___________princ_________") []
+    next_ident_away_in_goal (id_of_string "___________princ_________") []
   in
   begin
     Lemmas.start_proof
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0e51eb7e1b..64f9403a1c 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -383,7 +383,7 @@ let rec poseq_list_ids_rec lcstr gl =
 	      let _ = prconstr c in
 	      let _ = prstr "\n" in
 	      let typ = Tacmach.pf_type_of gl c in
-	      let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in
+	      let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in
 	      let x = Tactics.fresh_id [] cname gl in
 	      let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
 	      let _ = prstr " list_constr_largs = " in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 53359e31d7..fb1204c1f6 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -15,7 +15,7 @@ let msgnl m =
 let invalid_argument s = raise (Invalid_argument s)
 
 
-let fresh_id avoid s = Termops.next_global_ident_away true (id_of_string s) avoid
+let fresh_id avoid s = Namegen.next_ident_away_in_goal (id_of_string s) avoid
 
 let fresh_name avoid s = Name (fresh_id avoid s)
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ca93056ad1..ca608ec0ba 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -117,14 +117,12 @@ let generate_type g_to_f f graph i =
   in
   (*i We need to name the vars [res] and [fv] i*)
   let res_id =
-    Termops.next_global_ident_away
-      true
+    Namegen.next_ident_away_in_goal
       (id_of_string "res")
       (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt)
   in
   let fv_id =
-    Termops.next_global_ident_away
-      true
+    Namegen.next_ident_away_in_goal
       (id_of_string "fv")
       (res_id::(map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "Anonymous!") fun_ctxt))
   in
@@ -209,7 +207,7 @@ let rec generate_fresh_id x avoid i =
   if i == 0
   then []
   else
-    let id = Termops.next_global_ident_away true x avoid in
+    let id = Namegen.next_ident_away_in_goal x avoid in
     id::(generate_fresh_id x (id::avoid) (pred i))
 
 
@@ -271,7 +269,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
        environement and due to the bug #1174, we will need to pose the principle
        using a name
     *)
-    let principle_id = Termops.next_global_ident_away true (id_of_string "princ") ids in
+    let principle_id = Namegen.next_ident_away_in_goal (id_of_string "princ") ids in
     let ids = principle_id :: ids in
     (* We get the branches of the principle *)
     let branches = List.rev princ_infos.branches in
@@ -425,7 +423,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let params_bindings,avoid =
 	List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
+	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
 	     (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
@@ -435,7 +433,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let lemmas_bindings =
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
+	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
 	     (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 6dc36decf3..04e36d945d 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -77,7 +77,7 @@ let ident_global_exist id =
     global env) with base [id]. *)
 let next_ident_fresh (id:identifier) =
     let res = ref id in
-    while ident_global_exist !res do res := Nameops.lift_ident !res done;
+    while ident_global_exist !res do res := Nameops.lift_subscript !res done;
     !res
 
 
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 607734f222..752e546c89 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -138,7 +138,7 @@ let apply_args ctxt body args =
   let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) =
     match na with
        | Name id when List.mem id avoid ->
-	   let new_id = Nameops.next_ident_away id avoid in
+	   let new_id = Namegen.next_ident_away id avoid in
 	   Name new_id,Idmap.add id new_id mapping,new_id::avoid
        | _ -> na,mapping,avoid
   in
@@ -168,7 +168,7 @@ let apply_args ctxt body args =
 	    if need_convert_id avoid id
 	    then
 	      let new_avoid =  id::avoid in
-	      let new_id = Nameops.next_ident_away id new_avoid in
+	      let new_id = Namegen.next_ident_away id new_avoid in
 	      let new_avoid' = new_id :: new_avoid in
 	      let mapping = Idmap.add id new_id Idmap.empty in
 	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
@@ -550,7 +550,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		  match n with
 		    | Name id when List.exists (is_free_in id) args ->
 			(* need to alpha-convert the name *)
-			let new_id = Nameops.next_ident_away id avoid in
+			let new_id = Namegen.next_ident_away id avoid in
 			let new_avoid = id:: avoid in
 			let new_b =
 			  replace_var_by_term
diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml
index 502960a144..e31f1452d9 100644
--- a/plugins/funind/rawtermops.ml
+++ b/plugins/funind/rawtermops.ml
@@ -202,7 +202,7 @@ let rec alpha_pat excluded pat =
     | PatVar(loc,Name id) ->
 	if List.mem id excluded
 	then
-	  let new_id = Nameops.next_ident_away id excluded in
+	  let new_id = Namegen.next_ident_away id excluded in
 	  PatVar(loc,Name new_id),(new_id::excluded),
 	(Idmap.add id new_id Idmap.empty)
 	else pat,excluded,Idmap.empty
@@ -210,7 +210,7 @@ let rec alpha_pat excluded pat =
 	let new_na,new_excluded,map =
 	  match na with
 	    | Name id when List.mem id excluded ->
-		let new_id = Nameops.next_ident_away id excluded in
+		let new_id = Namegen.next_ident_away id excluded in
 		Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty
 	    | _ -> na,excluded,Idmap.empty
 	in
@@ -264,7 +264,7 @@ let rec alpha_rt excluded rt =
     match rt with
       | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
       | RLambda(loc,Anonymous,k,t,b) ->
-	  let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in
+	  let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in
 	  let new_excluded = new_id :: excluded in
 	  let new_t = alpha_rt new_excluded t in
 	  let new_b = alpha_rt new_excluded b in
@@ -278,7 +278,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt excluded b in
 	RLetIn(loc,Anonymous,new_t,new_b)
     | RLambda(loc,Name id,k,t,b) ->
-	let new_id = Nameops.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
 	  if new_id = id
 	  then t,b
@@ -291,7 +291,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded b in
 	RLambda(loc,Name new_id,k,new_t,new_b)
     | RProd(loc,Name id,k,t,b) ->
-	let new_id = Nameops.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id excluded in
 	let new_excluded = new_id::excluded in
 	let t,b =
 	  if new_id = id
@@ -304,7 +304,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded b in
 	RProd(loc,Name new_id,k,new_t,new_b)
     | RLetIn(loc,Name id,t,b) ->
-	let new_id = Nameops.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
 	  if new_id = id
 	  then t,b
@@ -325,7 +325,7 @@ let rec alpha_rt excluded rt =
 	       match na with
 		 | Anonymous -> (na::nal,excluded,mapping)
 		 | Name id ->
-		     let new_id = Nameops.next_ident_away id excluded in
+		     let new_id = Namegen.next_ident_away id excluded in
 		     if new_id = id
 		     then
 		       na::nal,id::excluded,mapping
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d64b9728b4..469f87f15b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -12,6 +12,7 @@
 
 open Term
 open Termops
+open Namegen
 open Environ
 open Declarations
 open Entries
@@ -50,7 +51,7 @@ open Genarg
 
 
 let compute_renamed_type gls c =
-  rename_bound_var (pf_env gls) [] (pf_type_of gls c)
+  rename_bound_vars_as_displayed (pf_env gls) [] (pf_type_of gls c)
 
 let qed () = Lemmas.save_named true
 let defined () = Lemmas.save_named false
@@ -58,7 +59,7 @@ let defined () = Lemmas.save_named false
 let pf_get_new_ids idl g =
   let ids = pf_ids_of_hyps g in
   List.fold_right
-    (fun id acc -> next_global_ident_away false id (acc@ids)::acc)
+    (fun id acc -> next_global_ident_away id (acc@ids)::acc)
     idl
     []
 
@@ -515,11 +516,11 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
       fun g ->
 	let ids = pf_ids_of_hyps g in
 	let s_max = mkApp(delayed_force coq_S, [|bound|]) in
-	let k = next_global_ident_away true k_id ids in
+	let k = next_ident_away_in_goal k_id ids in
         let ids = k::ids in
-	let h' = next_global_ident_away true (h'_id) ids in
+	let h' = next_ident_away_in_goal (h'_id) ids in
         let ids = h'::ids in
-	let def = next_global_ident_away true def_id ids in
+	let def = next_ident_away_in_goal def_id ids in
 	tclTHENLIST
 	  [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max]));
 	   observe_tac "introduce_all_equalities_final intro k" (h_intro  k);
@@ -543,15 +544,15 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
   | spec1::specs ->
       fun g ->
 	let ids = ids_of_named_context (pf_hyps g) in
-	let p = next_global_ident_away true p_id ids in
+	let p = next_ident_away_in_goal p_id ids in
         let ids = p::ids in
-	let pmax = next_global_ident_away true pmax_id ids in
+	let pmax = next_ident_away_in_goal pmax_id ids in
         let ids = pmax::ids in
-	let hle1 = next_global_ident_away true hle_id ids in
+	let hle1 = next_ident_away_in_goal hle_id ids in
         let ids = hle1::ids in
-	let hle2 = next_global_ident_away true  hle_id ids in
+	let hle2 = next_ident_away_in_goal  hle_id ids in
 	let ids = hle2::ids in
-	let heq = next_global_ident_away true heq_id ids in
+	let heq = next_ident_away_in_goal heq_id ids in
 	tclTHENLIST
 	  [simplest_elim (mkVar spec1);
 	   list_rewrite true eqs;
@@ -589,9 +590,9 @@ let rec introduce_all_values concl_tac is_mes acc_inv func context_fn
   | arg::args ->
       (fun g ->
 	let ids = ids_of_named_context (pf_hyps g) in
-	let rec_res = next_global_ident_away true rec_res_id ids in
+	let rec_res = next_ident_away_in_goal rec_res_id ids in
         let ids = rec_res::ids in
-	let hspec = next_global_ident_away true hspec_id ids in
+	let hspec = next_ident_away_in_goal hspec_id ids in
 	let tac =
 	  observe_tac "introduce_all_values" (
 	    introduce_all_values concl_tac is_mes acc_inv func context_fn eqs
@@ -722,13 +723,13 @@ let termination_proof_header is_mes input_type ids args_id relation
       in
       let relation = substl pre_rec_args relation in
       let input_type = substl pre_rec_args input_type in
-      let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in
+      let wf_thm = next_ident_away_in_goal (id_of_string ("wf_R")) ids in
       let wf_rec_arg =
-	next_global_ident_away true
+	next_ident_away_in_goal
 	  (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
 	  (wf_thm::ids)
       in
-      let hrec = next_global_ident_away true hrec_id
+      let hrec = next_ident_away_in_goal hrec_id
 	(wf_rec_arg::wf_thm::ids) in
       let acc_inv =
 	  lazy (
@@ -806,7 +807,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
       let (f_name, _, body1) = destLambda func_body in
       let f_id =
 	match f_name with
-	  | Name f_id -> next_global_ident_away true f_id ids
+	  | Name f_id -> next_ident_away_in_goal f_id ids
 	  | Anonymous -> anomaly "Anonymous function"
       in
       let n_names_types,_ = decompose_lam_n nb_args body1 in
@@ -815,7 +816,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 	  (fun (n_ids,ids) (n_name,_) ->
 	     match n_name with
 	       | Name id ->
-		   let n_id = next_global_ident_away true id ids in
+		   let n_id = next_ident_away_in_goal id ids in
 		   n_id::n_ids,n_id::ids
 	       | _ -> anomaly "anonymous argument"
 	  )
@@ -906,7 +907,7 @@ let build_new_goal_type () =
     (*
 let prove_with_tcc lemma _ : tactic =
   fun gls ->
-    let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+    let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
     tclTHENSEQ
       [
 	h_generalize [lemma];
@@ -930,7 +931,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
   in
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
-  let na = next_global_ident_away false name [] in
+  let na = next_global_ident_away name [] in
   if occur_existential gls_type then
     Util.error "\"abstract\" cannot handle existentials";
   let hook _ _ =
@@ -951,7 +952,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None);
     build_proof
       (  fun gls ->
-	   let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
 	   tclTHENSEQ
 	     [
 	       h_generalize [lemma];
@@ -1075,7 +1076,7 @@ let (value_f:constr list -> global_reference -> constr) =
       (
 	List.fold_left
 	  (fun x_id_l _ ->
-	     let x_id = next_global_ident_away true x_id x_id_l in
+	     let x_id = next_ident_away_in_goal x_id x_id_l in
 	     x_id::x_id_l
 	  )
 	  []
@@ -1122,7 +1123,7 @@ let (declare_f : identifier -> logical_kind -> constr list -> global_reference -
 
 let rec n_x_id ids n =
   if n = 0 then []
-  else let x = next_global_ident_away true x_id ids in
+  else let x = next_ident_away_in_goal x_id ids in
           x::n_x_id (x::ids) (n-1);;
 
 let start_equation (f:global_reference) (term_f:global_reference)
@@ -1141,12 +1142,12 @@ let start_equation (f:global_reference) (term_f:global_reference)
 
 let base_leaf_eq func eqs f_id g =
   let ids = pf_ids_of_hyps g in
-  let k = next_global_ident_away true k_id ids in
-  let p = next_global_ident_away true p_id (k::ids) in
-  let v = next_global_ident_away true v_id (p::k::ids) in
-  let heq = next_global_ident_away true heq_id (v::p::k::ids) in
-  let heq1 = next_global_ident_away true heq_id (heq::v::p::k::ids) in
-  let hex = next_global_ident_away true hex_id (heq1::heq::v::p::k::ids) in
+  let k = next_ident_away_in_goal k_id ids in
+  let p = next_ident_away_in_goal p_id (k::ids) in
+  let v = next_ident_away_in_goal v_id (p::k::ids) in
+  let heq = next_ident_away_in_goal heq_id (v::p::k::ids) in
+  let heq1 = next_ident_away_in_goal heq_id (heq::v::p::k::ids) in
+  let hex = next_ident_away_in_goal hex_id (heq1::heq::v::p::k::ids) in
     tclTHENLIST [
       h_intros [v; hex];
       simplest_elim (mkVar hex);
@@ -1168,7 +1169,7 @@ let rec introduce_all_values_eq cont_tac functional termine
     f p heq1 pmax bounds le_proofs eqs ids =
   function
       [] ->
-       let heq2 = next_global_ident_away true heq_id ids in
+       let heq2 = next_ident_away_in_goal heq_id ids in
 	tclTHENLIST
 	  [pose_proof (Name heq2)
              (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
@@ -1193,21 +1194,21 @@ let rec introduce_all_values_eq cont_tac functional termine
 	      tclTHENLIST[apply (delayed_force le_lt_SS);
 			compute_le_proofs le_proofs]]]
     | arg::args ->
-	let v' = next_global_ident_away true v_id ids in
+	let v' = next_ident_away_in_goal v_id ids in
         let ids = v'::ids in
-	let hex' = next_global_ident_away true hex_id ids in
+	let hex' = next_ident_away_in_goal hex_id ids in
         let ids = hex'::ids in
-	let p' = next_global_ident_away true p_id ids in
+	let p' = next_ident_away_in_goal p_id ids in
         let ids = p'::ids in
-	let new_pmax = next_global_ident_away true pmax_id ids in
+	let new_pmax = next_ident_away_in_goal pmax_id ids in
         let ids = pmax::ids in
-	let hle1 = next_global_ident_away true hle_id ids in
+	let hle1 = next_ident_away_in_goal hle_id ids in
         let ids = hle1::ids in
-	let hle2 = next_global_ident_away true hle_id ids in
+	let hle2 = next_ident_away_in_goal hle_id ids in
         let ids = hle2::ids in
-	let heq = next_global_ident_away true heq_id ids in
+	let heq = next_ident_away_in_goal heq_id ids in
         let ids = heq::ids in
-	let heq2 = next_global_ident_away true heq_id ids in
+	let heq2 = next_ident_away_in_goal heq_id ids in
         let ids = heq2::ids in
 	tclTHENLIST
 	  [mkCaseEq(mkApp(termine, Array.of_list arg));
@@ -1253,15 +1254,15 @@ let rec introduce_all_values_eq cont_tac functional termine
 
 
 let rec_leaf_eq termine f ids functional eqs expr fn args =
-  let p = next_global_ident_away true p_id ids in
+  let p = next_ident_away_in_goal p_id ids in
   let ids = p::ids in
-  let v = next_global_ident_away true v_id ids in
+  let v = next_ident_away_in_goal v_id ids in
   let ids = v::ids in
-  let hex = next_global_ident_away true hex_id ids in
+  let hex = next_ident_away_in_goal hex_id ids in
   let ids = hex::ids in
-  let heq1 = next_global_ident_away true heq_id ids in
+  let heq1 = next_ident_away_in_goal heq_id ids in
   let ids = heq1::ids in
-  let hle1 = next_global_ident_away true hle_id ids in
+  let hle1 = next_ident_away_in_goal hle_id ids in
   let ids = hle1::ids in
     tclTHENLIST
       [observe_tac "intros v hex" (h_intros [v;hex]);
diff --git a/plugins/interface/pbp.ml b/plugins/interface/pbp.ml
index b4dfe8a769..6032c3c000 100644
--- a/plugins/interface/pbp.ml
+++ b/plugins/interface/pbp.ml
@@ -21,12 +21,13 @@ open Libnames;;
 open Genarg;;
 open Topconstr;;
 open Termops;;
+open Namegen;;
 
 let zz = Util.dummy_loc;;
 
 let hyp_radix = id_of_string "H";;
 
-let next_global_ident = next_global_ident_away true
+let next_global_ident = next_ident_away_in_goal
 
 (* get_hyp_by_name : goal sigma -> string -> constr,
    looks up for an hypothesis (or a global constant), from its name *)
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 96bda6eccc..2db2533737 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 4eb05df74d..bc4d834d4f 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 26ac445c32..b96c587559 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 4dd3dd32be..8cf28a0dd6 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 *)
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 7706a3eb59..7f7bf5bf3c 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -571,7 +571,7 @@ print_endline "PASSATO" ; flush stdout ;
                    N.Anonymous
                   else
                    N.Name
-                    (Nameops.next_name_away n (Termops.ids_of_context env))
+                    (Namegen.next_name_away n (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id''
                 (string_of_sort innertype) ;
@@ -607,7 +607,7 @@ print_endline "PASSATO" ; flush stdout ;
                match n with
                   N.Anonymous -> N.Anonymous
                 | _ ->
-                  N.Name (Nameops.next_name_away n (Termops.ids_of_context env))
+                  N.Name (Namegen.next_name_away n (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                let sourcetype = CPropRetyping.get_type_of env evar_map s in
@@ -655,7 +655,7 @@ print_endline "PASSATO" ; flush stdout ;
                  | N.Name id -> id
               in
               let n' =
-               N.Name (Nameops.next_ident_away id (Termops.ids_of_context env))
+               N.Name (Namegen.next_ident_away id (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                let sourcesort =
@@ -771,7 +771,7 @@ print_endline "PASSATO" ; flush stdout ;
                   (function
                       N.Anonymous -> Util.error "Anonymous fix function met"
                     | N.Name id as n ->
-                       let res = N.Name (Nameops.next_name_away n !ids) in
+                       let res = N.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
                         res
                  ) f
@@ -805,7 +805,7 @@ print_endline "PASSATO" ; flush stdout ;
                   (function
                       N.Anonymous -> Util.error "Anonymous fix function met"
                     | N.Name id as n ->
-                       let res = N.Name (Nameops.next_name_away n !ids) in
+                       let res = N.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
                         res
                  ) f