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

13 files changed, 35 insertions, 320 deletions

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