Making Evd independent from Namegen.

5 files changed, 23 insertions, 22 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 0582e34be..e94fd72f1 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -418,6 +418,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
   let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
   let default_naming = Misctypes.IntroAnonymous in
   let naming = Option.default default_naming naming in
+  let name = match naming with
+  | Misctypes.IntroAnonymous -> None
+  | Misctypes.IntroIdentifier id -> Some id
+  | Misctypes.IntroFresh id ->
+    let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in
+    let id = Namegen.next_ident_away_from id has_name in
+    Some id
+  in
   let evi = {
     evar_hyps = sign;
     evar_concl = typ;
@@ -427,7 +435,7 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca
     evar_candidates = candidates;
     evar_extra = store; }
   in
-  let (evd, newevk) = Evd.new_evar evd ~naming evi in
+  let (evd, newevk) = Evd.new_evar evd ?name evi in
   let evd =
     if principal then Evd.declare_principal_goal newevk evd
     else Evd.declare_future_goal newevk evd
diff --git a/engine/evd.ml b/engine/evd.ml
index 3f00b91b6..b8f4b126a 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -365,7 +365,7 @@ open Misctypes
 type t
 
 val empty : t
-val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val add_name_undefined : Id.t option -> Evar.t -> evar_info -> t -> t
 val remove_name_defined : Evar.t -> t -> t
 val rename : Evar.t -> Id.t -> t -> t
 val reassign_name_defined : Evar.t -> Evar.t -> t -> t
@@ -379,20 +379,13 @@ type t = Id.t EvMap.t * existential_key Idmap.t
 
 let empty = (EvMap.empty, Idmap.empty)
 
-let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) =
-  let id = match naming with
-  | Misctypes.IntroAnonymous -> None
-  | Misctypes.IntroIdentifier id ->
-    if Idmap.mem id idtoev then
-    user_err  (str "Already an existential evar of name " ++ pr_id id);
-    Some id
-  | Misctypes.IntroFresh id ->
-    let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
-    Some id
-  in
+let add_name_newly_undefined id evk evi (evtoid, idtoev as names) =
   match id with
   | None -> names
-  | Some id -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+  | Some id ->
+    if Idmap.mem id idtoev then
+      user_err  (str "Already an existential evar of name " ++ pr_id id);
+    (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
 
 let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
   if EvMap.mem evk evtoid then
@@ -462,9 +455,9 @@ type evar_map = {
 let rename evk id evd =
   { evd with evar_names = EvNames.rename evk id evd.evar_names }
 
-let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with
+let add_with_name ?name d e i = match i.evar_body with
 | Evar_empty ->
-  let evar_names = EvNames.add_name_undefined naming e i d.evar_names in
+  let evar_names = EvNames.add_name_undefined name e i d.evar_names in
   { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
 | Evar_defined _ ->
   let evar_names = EvNames.remove_name_defined e d.evar_names in
@@ -481,9 +474,9 @@ let new_untyped_evar =
   let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
   fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
-let new_evar evd ?naming evi =
+let new_evar evd ?name evi =
   let evk = new_untyped_evar () in
-  let evd = add_with_name evd ?naming evk evi in
+  let evd = add_with_name evd ?name evk evi in
   (evd, evk)
 
 let remove d e =
diff --git a/engine/evd.mli b/engine/evd.mli
index fc1d4a514..2151000b6 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -149,7 +149,7 @@ val has_undefined : evar_map -> bool
     there are uninstantiated evars in [sigma]. *)
 
 val new_evar : evar_map ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> evar_info -> evar_map * evar
+  ?name:Id.t -> evar_info -> evar_map * evar
 (** Creates a fresh evar mapping to the given information. *)
 
 val add : evar_map -> evar -> evar_info -> evar_map
diff --git a/engine/sigma.ml b/engine/sigma.ml
index 9381a33af..001f8be80 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -29,8 +29,8 @@ let here x s = Sigma (x, s, ())
 
 type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
 
-let new_evar sigma ?naming info =
-  let (sigma, evk) = Evd.new_evar sigma ?naming info in
+let new_evar sigma ?name info =
+  let (sigma, evk) = Evd.new_evar sigma ?name info in
   Fresh (evk, sigma, ())
 
 let define evk c sigma =
diff --git a/engine/sigma.mli b/engine/sigma.mli
index 7473a251b..8e8df02f2 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -61,7 +61,7 @@ val to_evar : 'r evar -> Evar.t
 
 type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
 
-val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+val new_evar : 'r t -> ?name:Id.t ->
   Evd.evar_info -> 'r fresh
 
 val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma