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

3 files changed, 8 insertions, 41 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index c434be70d2..f82ef03e93 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 bc28ed98c2..28b799f530 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 10dfecc484..f69bf3ff03 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