From f52826877059858fb3fcd4314c629ed63d90a042 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 26 Sep 2015 19:50:41 +0200
Subject: 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.
---
 pretyping/evarutil.ml | 31 +++++++++++++------------------
 1 file changed, 13 insertions(+), 18 deletions(-)

(limited to 'pretyping/evarutil.ml')

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
-- 
cgit v1.2.3