Deprecate most evarutil evdref functions

clear_hyps remain with no alternative

6 files changed, 33 insertions, 10 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4c87b4e7ed..16244d8c0c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -295,7 +295,8 @@ let inductive_template evdref env tmloc ind =
         | LocalAssum (na,ty) ->
             let ty = EConstr.of_constr ty in
 	    let ty' = substl subst ty in
-	    let e = e_new_evar env evdref ~src:(hole_source n) ty' in
+            let evd, e = Evarutil.new_evar env !evdref ~src:(hole_source n) ty' in
+            evdref := evd;
 	    (e::subst,e::evarl,n+1)
 	| LocalDef (na,b,ty) ->
             let b = EConstr.of_constr b in
@@ -396,7 +397,9 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl =
 (* Utils *)
 
 let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref =
-  let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e
+  let evd, (e, u) = new_type_evar env !evdref univ_flexible_alg ~src:src in
+  evdref := evd;
+  e
 
 let evd_comb2 f evdref x y =
   let (evd',y) = f !evdref x y in
@@ -1681,7 +1684,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context env) in
-        let ev' = e_new_evar env evdref ~src ty in
+        let evd, ev' = Evarutil.new_evar env !evdref ~src ty in
+        evdref := evd;
         begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
@@ -1712,7 +1716,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	  (named_context extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = u :: List.map mkRel vl in
-      let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in
+      let evd, ev = Evarutil.new_evar extenv !evdref ~src ~filter ~candidates ty in
+      evdref := evd;
       lift k ev
   in
   aux (0,extenv,subst0) t0
@@ -1724,8 +1729,9 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
            we are in an impossible branch *)
 	let n = Context.Rel.length (rel_context env) in
 	let n' = Context.Rel.length (rel_context tycon_env) in
-	let impossible_case_type, u =
-	  e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in
+        let evd, (impossible_case_type, u) =
+          new_type_evar (reset_context env) !evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in
+        evdref := evd;
 	(lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6dc3687a0a..e8b17d694d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -94,7 +94,9 @@ open Program
 
 let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
   let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
-  Evarutil.e_new_evar env evdref ~src c
+  let evd, v = Evarutil.new_evar env !evdref ~src c in
+  evdref := evd;
+  v
 
 let app_opt env evdref f t =
   whd_betaiota !evdref (app_opt f t)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 144166a343..2144639d50 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1394,6 +1394,16 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
   | Success evd' -> evd'
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
+let make_opt = function
+  | Success evd -> Some evd
+  | UnifFailure _ -> None
+
+let conv env ?(ts=default_transparent_state env) evd t1 t2 =
+  make_opt(evar_conv_x ts env evd CONV t1 t2)
+
+let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
+  make_opt(evar_conv_x ts env evd CUMUL t1 t2)
+
 let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 =
   match evar_conv_x ts env !evdref CONV t1 t2 with
   | Success evd' -> evdref := evd'; true
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9270d6e3aa..da2b4d1b81 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -30,6 +30,9 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma
 val e_conv  : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
 val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
 
+val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
+val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
+
 (** {6 Unification heuristics. } *)
 
 (** Try heuristics to solve pending unification problems and to solve
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 52d940d8eb..8cfb7966cb 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -16,7 +16,9 @@ let init_reference dir s () = Coqlib.coq_reference  "Program" dir s
 let papp evdref r args = 
   let open EConstr in
   let gr = delayed_force r in
-    mkApp (Evarutil.e_new_global evdref gr, args)
+  let evd, hd = Evarutil.new_global !evdref gr in
+  evdref := evd;
+  mkApp (hd, args)
 
 let sig_typ = init_reference ["Init"; "Specif"] "sig"
 let sig_intro = init_reference ["Init"; "Specif"] "exist"
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d98ce9abab..1caa629ffb 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -198,8 +198,8 @@ let pose_all_metas_as_evars env evd t =
           then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
           else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
         let src = Evd.evar_source_of_meta mv !evdref in
-        let ev = Evarutil.e_new_evar env evdref ~src ty in
-        evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
+        let evd, ev = Evarutil.new_evar env !evdref ~src ty in
+        evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd;
         ev)
   | _ ->
       EConstr.map !evdref aux t in