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

68 files changed, 212 insertions, 502 deletions

diff --git a/dev/base_include b/dev/base_include
index d26d5b4db..3a31230f1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -90,6 +90,7 @@ open Evarutil
 open Tacred
 open Evd
 open Termops
+open Namegen
 open Indrec
 open Typing
 open Inductiveops
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 505141dd6..7c5b03457 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,16 @@
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================
 
+** Renaming functions renamed
+
+concrete_name -> compute_displayed_name_in
+concrete_let_name -> compute_displayed_let_name_in
+rename_rename_bound_var -> rename_bound_vars_as_displayed
+lookup_name_as_renamed -> lookup_name_as_displayed
+next_global_ident_away true -> next_ident_away_in_goal
+next_global_ident_away false -> next_global_ident_away
+
+
 ** Cleaning in commmand.ml
 
 Functions about starting/ending a lemma are in lemmas.ml
diff --git a/dev/printers.mllib b/dev/printers.mllib
index b5a54a189..d9f66d7bd 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -64,6 +64,7 @@ Goptions
 Decls
 Heads
 Termops
+Namegen
 Evd
 Rawterm
 Reductionops
diff --git a/ide/coq.ml b/ide/coq.ml
index b9257de84..bf1140552 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -24,6 +24,7 @@ open Hipattern
 open Tacmach
 open Reductionops
 open Termops
+open Namegen
 open Ideutils
 
 let prerr_endline s = if !debug then prerr_endline s else ()
@@ -635,7 +636,7 @@ let make_cases s =
 	     let rec rename avoid = function
 	       | [] -> []
 	       | (n,_)::l ->
-		   let n' = next_global_ident_away true
+		   let n' = next_ident_away_in_goal
 			      (id_of_name n)
 			      avoid
 		   in (string_of_id n')::(rename (n'::avoid) l)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fc607e354..e948dc6b4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -16,6 +16,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Namegen
 open Inductive
 open Sign
 open Environ
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 36a219a61..d8cb8c715 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -13,6 +13,7 @@ open Util
 open Flags
 open Names
 open Nameops
+open Namegen
 open Libnames
 open Impargs
 open Rawterm
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index f9ac88e6b..123998411 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -203,7 +203,7 @@ let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty)
       vars
 
 let rec make_fresh ids env x =
-  if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
+  if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_subscript x)
 
 let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a233d0be1..8f6a619a0 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -221,13 +221,17 @@ let vars_of_global env constr =
     | Const kn -> lookup_constant_variables kn env
     | Ind ind -> lookup_inductive_variables ind env
     | Construct cstr -> lookup_constructor_variables cstr env
-    | _ -> []
+    | _ -> raise Not_found
 
 let global_vars_set env constr =
   let rec filtrec acc c =
-    let vl = vars_of_global env c in
-    let acc = List.fold_right Idset.add vl acc in
-      fold_constr filtrec acc c
+    let acc =
+      match kind_of_term c with
+      | Var _ | Const _ | Ind _ | Construct _ ->
+	  List.fold_right Idset.add (vars_of_global env c) acc
+      | _ ->
+	  acc in
+    fold_constr filtrec acc c
   in
     filtrec Idset.empty constr
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 9401ba6b0..315bddd1f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -164,7 +164,7 @@ val set_engagement : engagement -> env -> env
 (* [global_vars_set env c] returns the list of [id]'s occurring as
    [VAR id] in [c] *)
 val global_vars_set : env -> constr -> Idset.t
-(* the constr must be an atomic construction *)
+(* the constr must be a global reference *)
 val vars_of_global : env -> constr -> identifier list
 
 val keep_hyps : env -> Idset.t -> section_context
diff --git a/library/impargs.ml b/library/impargs.ml
index c434be70d..f82ef03e9 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -22,6 +22,7 @@ open Nametab
 open Pp
 open Topconstr
 open Termops
+open Namegen
 
 (*s Flags governing the computation of implicit arguments *)
 
@@ -199,20 +200,15 @@ let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
 
 (* calcule la liste des arguments implicites *)
 
-let concrete_name avoid_flags l env_names n all c =
-  if n = Anonymous & noccurn 1 c then
-    (Anonymous,l)
-  else
-    let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
-    let idopt = if not all && noccurn 1 c then Anonymous else Name fresh_id in
-    (idopt, fresh_id::l)
+let find_displayed_name_in all =
+  if all then compute_and_force_displayed_name_in else compute_displayed_name_in
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rec aux env avoid n names t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
-	  let na',avoid' = concrete_name None avoid names na all b in
+	  let na',avoid' = find_displayed_name_in all None avoid names na b in
 	  add_free_rels_until strict strongly_strict revpat n env a (Hyp (n+1))
             (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ ->
@@ -224,7 +220,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   in
   match kind_of_term (whd_betadeltaiota env t) with
     | Prod (na,a,b) ->
-	let na',avoid = concrete_name None [] [] na all b in
+	let na',avoid = find_displayed_name_in all None [] [] na b in
 	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
 	Array.to_list v
     | _ -> []
diff --git a/library/nameops.ml b/library/nameops.ml
index bc28ed98c..28b799f53 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -112,26 +112,8 @@ let add_prefix s id = id_of_string (s ^ string_of_id id)
 
 let atompart_of_id id = fst (repr_ident id)
 
-(* Fresh names *)
-
 let lift_ident = lift_subscript
 
-let next_ident_away id avoid =
-  if List.mem id avoid then
-    let id0 = if not (has_subscript id) then id else
-    (* Ce serait sans doute mieux avec quelque chose inspiré de
-       *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
-    forget_subscript id in
-    let rec name_rec id =
-      if List.mem id avoid then name_rec (lift_ident id) else id in
-    name_rec id0
-  else id
-
-let next_ident_away_from id avoid =
-  let rec name_rec id =
-    if List.mem id avoid then name_rec (lift_ident id) else id in
-  name_rec id
-
 (* Names *)
 
 let out_name = function
@@ -158,13 +140,6 @@ let name_fold_map f e = function
   | Name id -> let (e,id) = f e id in (e,Name id)
   | Anonymous -> e,Anonymous
 
-let next_name_away_with_default default name l =
-  match name with
-    | Name str  -> next_ident_away str l
-    | Anonymous -> next_ident_away (id_of_string default) l
-
-let next_name_away = next_name_away_with_default "H"
-
 let pr_lab l = str (string_of_label l)
 
 let default_library = Names.initial_dir (* = ["Top"] *)
diff --git a/library/nameops.mli b/library/nameops.mli
index 10dfecc48..f69bf3ff0 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -23,13 +23,9 @@ val root_of_id : identifier -> identifier (* remove trailing digits, $'$ and $\_
 val add_suffix : identifier -> string -> identifier
 val add_prefix : string -> identifier -> identifier
 
-val lift_ident           : identifier -> identifier
-val next_ident_away      : identifier -> identifier list -> identifier
-val next_ident_away_from : identifier -> identifier list -> identifier
-
-val next_name_away : name -> identifier list -> identifier
-val next_name_away_with_default :
-  string -> name -> identifier list -> identifier
+val has_subscript    : identifier -> bool
+val lift_subscript   : identifier -> identifier
+val forget_subscript : identifier -> identifier
 
 val out_name : name -> identifier
 
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 0c815d262..25b17814f 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -52,6 +52,7 @@ Goptions
 Decl_kinds
 Global
 Termops
+Namegen
 Evd
 Reductionops
 Inductiveops
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index a0c9a15ad..58df67424 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -10,7 +10,7 @@
 
 open Pp
 open Names
-open Nameops
+open Namegen
 open Util
 open Tacexpr
 open Rawterm
@@ -626,7 +626,7 @@ let pr_fix_tac (id,n,c) =
           match list_chop (n-1) nal with
               _, (_,Name id) :: _ -> id, (nal,ty)::bll
             | bef, (loc,Anonymous) :: aft ->
-                let id = next_ident_away_from (id_of_string"y") avoid in
+                let id = next_ident_away (id_of_string"y") avoid in
                 id, ((bef@(loc,Name id)::aft, ty)::bll)
             | _ -> assert false
         else
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 80f05bf92..eb6e88c97 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -19,7 +19,7 @@ let get_new_id locals id =
       if not (Nametab.exists_module dir) then
 	id
       else
-	get_id (id::l) (Nameops.next_ident_away id l)
+	get_id (id::l) (Namegen.next_ident_away id l)
   in
     get_id (List.map snd locals) id
 
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 636504361..46e5b50aa 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 47381f6d8..73b51cfe7 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 d119dbe8e..71bb634da 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 043bf0fe7..df9f02dfd 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 3d789b92e..e8ec962b4 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 ff4d1e972..b756492b5 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 0e51eb7e1..64f9403a1 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 53359e31d..fb1204c1f 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 ca93056ad..ca608ec0b 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 6dc36decf..04e36d945 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 607734f22..752e546c8 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 502960a14..e31f1452d 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 d64b9728b..469f87f15 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 b4dfe8a76..6032c3c00 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 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 *)
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 7706a3eb5..7f7bf5bf3 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
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7fa80b9a4..fbc8bcd07 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -13,6 +13,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Namegen
 open Declarations
 open Inductiveops
 open Environ
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 9ce46ab8a..e838cb2e0 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Namegen
 open Sign
 open Environ
 open Evd
@@ -145,7 +146,7 @@ let mk_clenv_from_n gls n (c,cty) =
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
 let mk_clenv_rename_from_n gls n (c,t) =
-  mk_clenv_from_n gls n (c,rename_bound_var (pf_env gls) [] t)
+  mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed (pf_env gls) [] t)
 
 let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0d94838f0..c152f3ca8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -21,6 +21,7 @@ open Sign
 open Rawterm
 open Nameops
 open Termops
+open Namegen
 open Libnames
 open Nametab
 open Evd
@@ -169,16 +170,16 @@ let computable p k =
 
 let avoid_flag isgoal = if isgoal then Some true else None
 
-let lookup_name_as_renamed env t s =
+let lookup_name_as_displayed env t s =
   let rec lookup avoid env_names n c = match kind_of_term c with
     | Prod (name,_,c') ->
-	(match concrete_name (Some true) avoid env_names name c' with
+	(match compute_displayed_name_in (Some true) avoid env_names name c' with
            | (Name id,avoid') ->
 	       if id=s then (Some n)
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
 	   | (Anonymous,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
     | LetIn (name,_,_,c') ->
-	(match concrete_name (Some true) avoid env_names name c' with
+	(match compute_displayed_name_in (Some true) avoid env_names name c' with
            | (Name id,avoid') ->
 	       if id=s then (Some n)
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
@@ -190,7 +191,7 @@ let lookup_name_as_renamed env t s =
 let lookup_index_as_renamed env t n =
   let rec lookup n d c = match kind_of_term c with
     | Prod (name,_,c') ->
-	  (match concrete_name (Some true) [] empty_names_context name c' with
+	  (match compute_displayed_name_in (Some true) [] empty_names_context name c' with
                (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if n=0 then
@@ -200,7 +201,7 @@ let lookup_index_as_renamed env t n =
 		 else
 		   lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
-	  (match concrete_name (Some true) [] empty_names_context name c' with
+	  (match compute_displayed_name_in (Some true) [] empty_names_context name c' with
              | (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if n=0 then
@@ -229,11 +230,11 @@ let rec decomp_branch n nal b (avoid,env as e) c =
   else
     let na,c,f =
       match kind_of_term (strip_outer_cast c) with
-	| Lambda (na,_,c) -> na,c,concrete_let_name
-	| LetIn (na,_,_,c) -> na,c,concrete_name
+	| Lambda (na,_,c) -> na,c,compute_displayed_let_name_in
+	| LetIn (na,_,_,c) -> na,c,compute_displayed_name_in
 	| _ ->
 	    Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])),
-	    concrete_name in
+	    compute_displayed_name_in in
     let na',avoid' = f (Some b) avoid env na c in
     decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c
 
@@ -294,7 +295,7 @@ let it_destRLambda_or_LetIn_names n c =
       | _ ->
           (* eta-expansion *)
 	  let rec next l =
-	    let x = Nameops.next_ident_away (id_of_string "x") l in
+	    let x = next_ident_away (id_of_string "x") l in
 	    (* Not efficient but unusual and no function to get free rawvars *)
 (* 	    if occur_rawconstr x c then next (x::l) else x in *)
 	    x
@@ -534,9 +535,9 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
 and detype_binder isgoal bk avoid env na ty c =
   let na',avoid' =
     if bk = BLetIn then
-      concrete_let_name (avoid_flag isgoal) avoid env na c
+      compute_displayed_let_name_in (avoid_flag isgoal) avoid env na c
     else
-      concrete_name (avoid_flag isgoal) avoid env na c in
+      compute_displayed_name_in (avoid_flag isgoal) avoid env na c in
   let r =  detype isgoal avoid' (add_name na' env) c in
   match bk with
   | BProd -> RProd (dl, na',Explicit,detype isgoal avoid env ty, r)
@@ -552,8 +553,8 @@ let rec detype_rel_context where avoid env sign =
 	match where with
 	| None -> na,avoid
 	| Some c ->
-	    if b<>None then concrete_let_name None avoid env na c
-	    else concrete_name None avoid env na c in
+	    if b<>None then compute_displayed_let_name_in None avoid env na c
+	    else compute_displayed_name_in None avoid env na c in
       let b = Option.map (detype false avoid env) b in
       let t = detype false avoid env t in
       (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index d1e0d1049..d7fb01aec 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -44,7 +44,7 @@ val detype_rel_context : constr option -> identifier list -> names_context ->
   rel_context -> rawdecl list
 
 (* look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_renamed  : env -> constr -> identifier -> int option
+val lookup_name_as_displayed  : env -> constr -> identifier -> int option
 val lookup_index_as_renamed : env -> constr -> int -> int option
 
 val set_detype_anonymous : (loc -> int -> rawconstr) -> unit
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2c6d1c0b8..1357c6ce3 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -11,10 +11,10 @@
 open Util
 open Pp
 open Names
-open Nameops
 open Univ
 open Term
 open Termops
+open Namegen
 open Sign
 open Pre_env
 open Environ
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e7dbc1af6..1352b3830 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -19,6 +19,7 @@ open Libnames
 open Nameops
 open Term
 open Termops
+open Namegen
 open Declarations
 open Entries
 open Inductive
@@ -40,7 +41,7 @@ type recursion_scheme_error =
 
 exception RecursionSchemeError of recursion_scheme_error
 
-let make_prod_dep dep env = if dep then prod_name env else mkProd
+let make_prod_dep dep env = if dep then mkProd_name env else mkProd
 let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
 (*******************************************)
@@ -205,7 +206,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
       match kind_of_term p' with
 	| Prod (n,t,c) ->
 	    let d = (n,None,t) in
-	    lambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
+	    mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
 	| LetIn (n,b,t,c) ->
 	    let d = (n,Some b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
@@ -228,7 +229,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	in
         (match optionpos with
            | None ->
-	       lambda_name env
+	       mkLambda_name env
 		 (n,t,process_constr (push_rel d env) (i+1)
 		    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)])))
 		    (cprest,rest))
@@ -236,7 +237,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	       let nF = lift (i+1+decF) f_0 in
                let env' = push_rel d env in
 	       let arg = process_pos env' nF (lift 1 t) in
-               lambda_name env
+               mkLambda_name env
 		 (n,t,process_constr env' (i+1)
 		    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
 		    (cprest,rest)))
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1f196f43e..636f86224 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -13,6 +13,7 @@ open Names
 open Univ
 open Term
 open Termops
+open Namegen
 open Sign
 open Declarations
 open Environ
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index aa83f71c2..b44dd94ef 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -14,6 +14,7 @@ open Names
 open Sign
 open Term
 open Termops
+open Namegen
 open Environ
 open Type_errors
 open Rawterm
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index ab0fac4a6..b40476c97 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -2,6 +2,7 @@ Termops
 Evd
 Reductionops
 Vnorm
+Namegen
 Inductiveops
 Retyping
 Cbv
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a9732be47..7079b937b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -15,6 +15,7 @@ open Nameops
 open Term
 open Libnames
 open Termops
+open Namegen
 open Declarations
 open Inductive
 open Environ
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 3b6d13d47..81c740580 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -488,10 +488,11 @@ let occur_in_global env id constr =
   let vars = vars_of_global env constr in
   if List.mem id vars then raise Occur
 
-let occur_var env s c =
+let occur_var env id c =
   let rec occur_rec c =
-    occur_in_global env s c;
-    iter_constr occur_rec c
+    match kind_of_term c with
+    | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id c
+    | _ -> iter_constr occur_rec c
   in
   try occur_rec c; false with Occur -> true
 
@@ -694,11 +695,6 @@ let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,t
 	  if rest <> [] then error_invalid_occurrence rest;
 	  (id,Some body',t')
 
-(* First character of a constr *)
-
-let lowercase_first_char id =
-  lowercase_first_char_utf8 (string_of_id id)
-
 let vars_of_env env =
   let s =
     Sign.fold_named_context (fun (id,_,_) s -> Idset.add id s)
@@ -711,85 +707,6 @@ let add_vname vars = function
     Name id -> Idset.add id vars
   | _ -> vars
 
-let basename_of_global = Nametab.basename_of_global
-
-let sort_hdchar = function
-  | Prop(_) -> "P"
-  | Type(_) -> "T"
-
-let hdchar env c =
-  let rec hdrec k c =
-    match kind_of_term c with
-    | Prod (_,_,c)       -> hdrec (k+1) c
-    | Lambda (_,_,c)     -> hdrec (k+1) c
-    | LetIn (_,_,_,c)    -> hdrec (k+1) c
-    | Cast (c,_,_)         -> hdrec k c
-    | App (f,l)         -> hdrec k f
-    | Const kn       ->
-	lowercase_first_char (id_of_label (con_label kn))
-    | Ind ((kn,i) as x) ->
-	if i=0 then
-	  lowercase_first_char (id_of_label (mind_label kn))
-	else
-	  lowercase_first_char (basename_of_global (IndRef x))
-    | Construct ((sp,i) as x) ->
-	lowercase_first_char (basename_of_global (ConstructRef x))
-    | Var id  -> lowercase_first_char id
-    | Sort s -> sort_hdchar s
-    | Rel n ->
-	(if n<=k then "p" (* the initial term is flexible product/function *)
-	 else
-	   try match Environ.lookup_rel (n-k) env with
-	     | (Name id,_,_)   -> lowercase_first_char id
-	     | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
-	   with Not_found -> "y")
-    | Fix ((_,i),(lna,_,_)) ->
-	let id = match lna.(i) with Name id -> id | _ -> assert false in
-	lowercase_first_char id
-    | CoFix (i,(lna,_,_)) ->
-	let id = match lna.(i) with Name id -> id | _ -> assert false in
-	lowercase_first_char id
-    | Meta _|Evar _|Case (_, _, _, _) -> "y"
-  in
-  hdrec 0 c
-
-let id_of_name_using_hdchar env a = function
-  | Anonymous -> id_of_string (hdchar env a)
-  | Name id   -> id
-
-let named_hd env a = function
-  | Anonymous -> Name (id_of_string (hdchar env a))
-  | x         -> x
-
-let mkProd_name   env (n,a,b) = mkProd (named_hd env a n, a, b)
-let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
-
-let lambda_name = mkLambda_name
-let prod_name = mkProd_name
-
-let prod_create   env (a,b) = mkProd (named_hd env a Anonymous, a, b)
-let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous, a, b)
-
-let name_assumption env (na,c,t) =
-  match c with
-    | None      -> (named_hd env t na, None, t)
-    | Some body -> (named_hd env body na, c, t)
-
-let name_context env hyps =
-  snd
-    (List.fold_left
-       (fun (env,hyps) d ->
-	  let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
-       (env,[]) (List.rev hyps))
-
-let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
-let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
-
-let it_mkProd_or_LetIn_name env b hyps =
-  it_mkProd_or_LetIn ~init:b (name_context env hyps)
-let it_mkLambda_or_LetIn_name env b hyps =
-  it_mkLambda_or_LetIn ~init:b (name_context env hyps)
-
 (*************************)
 (*   Names environments  *)
 (*************************)
@@ -823,63 +740,10 @@ let ids_of_context env =
 let names_of_rel_context env =
   List.map (fun (na,_,_) -> na) (rel_context env)
 
-(**** Globality of identifiers *)
-
-let rec is_imported_modpath mp = 
-  let current_mp,_ = Lib.current_prefix() in
-    match mp with
-      | MPfile dp ->
-	  let rec find_prefix = function
-	    |MPfile dp1 -> not (dp1=dp)
-	    |MPdot(mp,_) -> find_prefix mp
-	    |MPbound(_) -> false
-	  in find_prefix current_mp
-      | p -> false
-
-let is_imported_ref = function
-  | VarRef _ -> false
-  | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) ->
-      let (mp,_,_) = repr_mind kn in is_imported_modpath mp
-  | ConstRef kn ->
-      let (mp,_,_) = repr_con kn in is_imported_modpath mp
-
-let is_global id =
-  try
-    let ref = locate (qualid_of_ident id) in
-    not (is_imported_ref ref)
-  with Not_found ->
-    false
-
-let is_constructor id =
-  try
-    match locate (qualid_of_ident id) with
-      | ConstructRef _ as ref -> not (is_imported_ref ref)
-      | _ -> false
-  with Not_found ->
-    false
-
 let is_section_variable id =
   try let _ = Global.lookup_named id in true
   with Not_found -> false
 
-let next_global_ident_from allow_secvar id avoid =
-  let rec next_rec id =
-    let id = next_ident_away_from id avoid in
-    if (allow_secvar && is_section_variable id) || not (is_global id) then
-      id
-    else
-      next_rec (lift_ident id)
-  in
-  next_rec id
-
-let next_global_ident_away allow_secvar id avoid =
-  let id  = next_ident_away id avoid in
-  if (allow_secvar && is_section_variable id) || not (is_global id) then
-    id
-  else
-    next_global_ident_from allow_secvar (lift_ident id) avoid
-
 let isGlobalRef c =
   match kind_of_term c with
   | Const _ | Ind _ | Construct _ | Var _ -> true
@@ -890,68 +754,6 @@ let has_polymorphic_type c =
   | Declarations.PolymorphicArity _ -> true
   | _ -> false
 
-(* nouvelle version de renommage des variables (DEC 98) *)
-(* This is the algorithm to display distinct bound variables
-
-    - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
-      des noms à éviter
-    - Règle 2 : c'est la dépendance qui décide si on affiche ou pas
-
-    Exemple :
-    si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors
-    il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
-    mais f et f0 contribue à la liste des variables à éviter (en supposant
-    que les noms f et f0 ne sont pas déjà pris)
-    Intérêt : noms homogènes dans un but avant et après Intro
-*)
-
-type used_idents = identifier list
-
-let occur_rel p env id =
-  try lookup_name_of_rel p env = Name id
-  with Not_found -> false (* Unbound indice : may happen in debug *)
-
-let occur_id nenv id0 c =
-  let rec occur n c = match kind_of_term c with
-    | Var id when  id=id0 -> raise Occur
-    | Const kn when basename_of_global (ConstRef kn) = id0 -> raise Occur
-    | Ind ind_sp
-	when basename_of_global (IndRef ind_sp) = id0 ->
-        raise Occur
-    | Construct cstr_sp
-	when basename_of_global (ConstructRef cstr_sp) = id0 ->
-        raise Occur
-    | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur
-    | _ -> iter_constr_with_binders succ occur n c
-  in
-  try occur 1 c; false
-  with Occur -> true
-    | Not_found -> false (* Case when a global is not in the env *)
-
-type avoid_flags = bool option
-
-let next_name_not_occuring avoid_flags name l env_names t =
-  let rec next id =
-    if List.mem id l or occur_id env_names id t or
-      (* Further restrictions ? *)
-      match avoid_flags with None -> false | Some not_only_cstr ->
-      (if not_only_cstr then
-	(* To be consistent with the intro mechanism *)
-	is_global id & not (is_section_variable id)
-      else
-	(* To avoid constructors in pattern-matchings *)
-	is_constructor id)
-    then next (lift_ident id)
-    else id
-  in
-  match name with
-    | Name id   -> next id
-    | Anonymous ->
-        (* Normally, an anonymous name is not dependent and will not be *)
-        (* taken into account by the function concrete_name; just in case *)
-        (* invent a valid name *)
-        next (id_of_string "H")
-
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
     | (Prop c1, Prop c2) -> c1 = Null or c2 = Pos  (* Prop <= Set *)
@@ -1129,15 +931,6 @@ let rec mem_named_context id = function
   | _ :: sign -> mem_named_context id sign
   | [] -> false
 
-let make_all_name_different env =
-  let avoid = ref (ids_of_named_context (named_context env)) in
-  process_rel_context
-    (fun (na,c,t) newenv ->
-       let id = next_name_away na !avoid in
-       avoid := id::!avoid;
-       push_rel (Name id,c,t) newenv)
-    env
-
 let global_vars env ids = Idset.elements (global_vars_set env ids)
 
 let global_vars_set_of_decl env = function
@@ -1159,43 +952,6 @@ let dependency_closure env sign hyps =
         sign in
     List.rev lh
 
-let default_x = id_of_string "x"
-
-let rec next_name_away_in_cases_pattern id avoid =
-  let id = match id with Name id -> id | Anonymous -> default_x in
-  let rec next id =
-    if List.mem id avoid or is_constructor id then next (lift_ident id)
-    else id in
-  next id
-
-(* Remark: Anonymous var may be dependent in Evar's contexts *)
-let concrete_name avoid_flags l env_names n c =
-  if n = Anonymous & noccurn 1 c then
-    (Anonymous,l)
-  else
-    let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
-    let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
-    (idopt, fresh_id::l)
-
-let concrete_let_name avoid_flags l env_names n c =
-  let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
-  (Name fresh_id, fresh_id::l)
-
-let rec rename_bound_var env avoid c =
-  let env_names = names_of_rel_context env in
-  let rec rename avoid c =
-    match kind_of_term c with
-    | Prod (na,c1,c2)  ->
-	let na',avoid' = concrete_name None avoid env_names na c2 in
-	mkProd (na', c1, rename avoid' c2)
-    | LetIn (na,c1,t,c2) ->
-	let na',avoid' = concrete_let_name None avoid env_names na c2 in
-	mkLetIn (na',c1,t, rename avoid' c2)
-    | Cast (c,k,t) -> mkCast (rename avoid c, k,t)
-    | _ -> c
-  in
-  rename avoid c
-
 (* Combinators on judgments *)
 
 let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index f28fee951..7f9ccb28e 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -101,7 +101,6 @@ val occur_existential : types -> bool
 val occur_meta_or_existential : types -> bool
 val occur_const : constant -> types -> bool
 val occur_evar : existential_key -> types -> bool
-val occur_in_global : env -> identifier -> constr -> unit
 val occur_var : env -> identifier -> types -> bool
 val occur_var_in_decl :
   env ->
@@ -194,31 +193,6 @@ val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
 val decompose_prod_letin : constr -> int * rel_context * constr
 val align_prod_letin : constr -> constr -> rel_context * constr
 
-(* finding "intuitive" names to hypotheses *)
-val lowercase_first_char : identifier -> string
-val sort_hdchar : sorts -> string
-val hdchar : env -> types -> string
-val id_of_name_using_hdchar :
-  env -> types -> name -> identifier
-val named_hd : env -> types -> name -> name
-
-val mkProd_name : env -> name * types * types -> types
-val mkLambda_name : env -> name * types * constr -> constr
-
-(* Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
-val prod_name : env -> name * types * types -> types
-val lambda_name : env -> name * types * constr -> constr
-
-val prod_create : env -> types * types -> constr
-val lambda_create : env -> types * constr -> constr
-val name_assumption : env -> rel_declaration -> rel_declaration
-val name_context : env -> rel_context -> rel_context
-
-val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types
-val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
-val it_mkProd_or_LetIn_name   : env -> types -> rel_context -> types
-val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
-
 (* Get the last arg of a constr intended to be an application *)
 val last_arg : constr -> constr
 
@@ -239,29 +213,6 @@ val context_chop : int -> rel_context -> (rel_context*rel_context)
 val vars_of_env: env -> Idset.t
 val add_vname : Idset.t -> name -> Idset.t
 
-(* sets of free identifiers *)
-type used_idents = identifier list
-val occur_rel : int -> name list -> identifier -> bool
-val occur_id : name list -> identifier -> constr -> bool
-
-type avoid_flags = bool option
- (* Some true = avoid all globals (as in intro);
-    Some false = avoid only global constructors; None = don't avoid globals *)
-
-val next_name_away_in_cases_pattern :
-  name -> identifier list -> identifier
-val next_global_ident_away :
-  (*allow section vars:*) bool -> identifier -> identifier list -> identifier
-val next_name_not_occuring :
-  avoid_flags -> name -> identifier list -> name list -> constr -> identifier
-val concrete_name :
-  avoid_flags -> identifier list -> name list -> name -> constr ->
-    name * identifier list
-val concrete_let_name :
-  avoid_flags -> identifier list -> name list -> name -> constr ->
-    name * identifier list
-val rename_bound_var : env -> identifier list -> types -> types
-
 (* other signature iterators *)
 val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : rel_context -> (name * constr) list
@@ -277,7 +228,6 @@ val fold_named_context_both_sides :
   ('a -> named_declaration -> named_declaration list -> 'a) ->
     named_context -> init:'a -> 'a
 val mem_named_context : identifier -> named_context -> bool
-val make_all_name_different : env -> env
 
 val global_vars : env -> constr -> identifier list
 val global_vars_set_of_decl : env -> named_declaration -> Idset.t
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a3e63541f..9156dfa9e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Namegen
 open Sign
 open Environ
 open Evd
@@ -49,8 +50,8 @@ let abstract_scheme env c l lname_typ =
 (* [occur_meta ta] test removed for support of eelim/ecase but consequences
    are unclear...
        if occur_meta ta then error "cannot find a type for the generalisation"
-       else *) if occur_meta a then lambda_name env (na,ta,t)
-       else lambda_name env (na,ta,subst_term_occ locc a t))
+       else *) if occur_meta a then mkLambda_name env (na,ta,t)
+       else mkLambda_name env (na,ta,subst_term_occ locc a t))
     c
     (List.rev l)
     lname_typ
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e8ef6dd67..7895bfac9 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -342,15 +342,18 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_by_tactic typ tac =
+let build_constant_by_tactic sign typ tac =
   let id = id_of_string ("temporary_proof"^string_of_int (next())) in
-  let sign = Decls.clear_proofs (Global.named_context ()) in
   start_proof id (Global,Proof Theorem) sign typ (fun _ _ -> ());
   try
     by tac;
     let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
     delete_current_proof ();
-    const.const_entry_body
+    const
   with e ->
     delete_current_proof ();
     raise e
+
+let build_by_tactic typ tac =
+  let sign = Decls.clear_proofs (Global.named_context ()) in
+  (build_constant_by_tactic sign typ tac).const_entry_body
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f46825b0c..6acf1ff78 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -197,4 +197,6 @@ val mutate : (pftreestate -> pftreestate) -> unit
 
 (* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
 
+val build_constant_by_tactic : named_context_val -> types -> tactic ->
+  Entries.definition_entry
 val build_by_tactic : types -> tactic -> constr
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index b5f46d788..8c808e1c8 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -68,8 +68,8 @@ let is_tactic_proof pf = match pf.ref with
   | _ -> false
 
 
-let pf_lookup_name_as_renamed env ccl s =
-  Detyping.lookup_name_as_renamed env ccl s
+let pf_lookup_name_as_displayed env ccl s =
+  Detyping.lookup_name_as_displayed env ccl s
 
 let pf_lookup_index_as_renamed env ccl n =
   Detyping.lookup_index_as_renamed env ccl n
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index dcbddbd9e..6d1fc143d 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -33,7 +33,7 @@ val is_complete_proof : proof_tree -> bool
 val is_leaf_proof     : proof_tree -> bool
 val is_tactic_proof   : proof_tree -> bool
 
-val pf_lookup_name_as_renamed  : env -> constr -> identifier -> int option
+val pf_lookup_name_as_displayed  : env -> constr -> identifier -> int option
 val pf_lookup_index_as_renamed : env -> constr -> int -> int option
 
 val is_proof_instr : rule -> bool
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 754d98616..acccfb812 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -11,7 +11,7 @@
 open Pp
 open Util
 open Names
-open Nameops
+open Namegen
 open Sign
 open Term
 open Termops
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 =
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 063fe7a10..8412a39f3 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -170,7 +170,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	    id
       | Anonymous ->
 	  let i = Nameops.add_suffix (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
   evars := Evarutil.nf_evar_defs !evars;
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 6b8c45fec..c769e8930 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -13,6 +13,7 @@ open Util
 open Flags
 open Names
 open Nameops
+open Namegen
 open Term
 open Termops
 open Inductive
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 7ea001259..d9a26b427 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -26,6 +26,7 @@ open Decl_kinds
 open Declare
 open Pretyping
 open Termops
+open Namegen
 open Evd
 open Evarutil
 open Reductionops
@@ -175,7 +176,7 @@ let compute_proof_name = function
       id
   | None ->
       let rec next avoid id =
-        let id = next_global_ident_away false id avoid in
+        let id = next_global_ident_away id avoid in
         if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id
         else id
       in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 1a3e5102e..5ed989438 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -162,7 +162,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
   let r = mkInd indsp in
   let rp = applist (r, extended_rel_list 0 paramdecls) in
   let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
-  let x = match name with Some n -> Name n | None -> Termops.named_hd (Global.env()) r Anonymous in
+  let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in
   let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
   let lifted_fields = lift_rel_context 1 fields in
   let (_,kinds,sp_projs,_) =
@@ -332,7 +332,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
 	cref, [proj_name, Some proj_cst]
     | _ ->
-	let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
+	let idarg = Namegen.next_ident_away (snd id) (ids_of_context (Global.env())) in
 	let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls
 	  params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
 	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3d7751d97..e3aa41354 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -153,7 +153,7 @@ let make_cases s =
 	     let rec rename avoid = function
 	       | [] -> []
 	       | (n,_)::l ->
-		   let n' = Termops.next_global_ident_away true (id_of_name n) avoid in
+		   let n' = Namegen.next_ident_away_in_goal (id_of_name n) avoid in
 		   string_of_id n' :: rename (n'::avoid) l in
 	     let al' = rename [] (List.rev al) in
 	     (string_of_id n :: al') :: l)