Hardening the API of evarmaps.

The evar counter has been moved from Evarutil to Evd, and all functions in
Evarutil now go through a dedicated primitive to create a fresh evar from
an evarmap.

1 files changed, 13 insertions, 18 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ee6bbe7fb..6684b0604 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -239,17 +239,6 @@ let make_pure_subst evi args =
         | _ -> anomaly (Pp.str "Instance does not match its signature"))
     (evar_filtered_context evi) (Array.rev_to_list args,[]))
 
-(**********************)
-(* Creating new evars *)
-(**********************)
-
-let evar_counter_summary_name = "evar counter"
-
-(* Generator of existential names *)
-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
-
 (*------------------------------------*
  * functional operations on evar sets *
  *------------------------------------*)
@@ -354,17 +343,15 @@ let push_rel_context_to_named_context env typ =
 let default_source = (Loc.ghost,Evar_kinds.InternalHole)
 
 let restrict_evar evd evk filter candidates =
-  let evk' = new_untyped_evar () in
-  let evd = Evd.restrict evk evk' filter ?candidates evd in
+  let evd, evk' = Evd.restrict evk filter ?candidates evd in
   Evd.declare_future_goal evk' evd, evk'
 
 let new_pure_evar_full evd evi =
-  let evk = new_untyped_evar () in
-  let evd = Evd.add evd evk evi in
+  let (evd, evk) = Evd.new_evar evd evi in
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?naming ?(principal=false) typ =
+let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
   let default_naming =
     if principal then
         (* waiting for a more principled approach
@@ -374,8 +361,16 @@ let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?nam
         Misctypes.IntroAnonymous
   in
   let naming = Option.default default_naming naming in
-  let newevk = new_untyped_evar() in
-  let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in
+  let evi = {
+    evar_hyps = sign;
+    evar_concl = typ;
+    evar_body = Evar_empty;
+    evar_filter = filter;
+    evar_source = src;
+    evar_candidates = candidates;
+    evar_extra = store; }
+  in
+  let (evd, newevk) = Evd.new_evar evd ~naming evi in
   let evd =
     if principal then Evd.declare_principal_goal newevk evd
     else Evd.declare_future_goal newevk evd