[api] Deprecate `evar_map` ref combinators.

All the `evar_map` APIs were deprecated in 8.9, thus we deprecate the
combinators to discourage this style of programming.

Still a few places do use imperative style, but they are pretty
localized and should be cleaned up separately.

As these are the last bits of `e_` API remaining this PR closes #6342.

1 files changed, 10 insertions, 5 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index f718b13a63..5ac4284b43 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -70,6 +70,11 @@ type inversion_kind =
   | FullInversion
   | FullInversionClear
 
+let evd_comb1 f evdref x =
+  let (evd',y) = f !evdref x in
+  evdref := evd';
+  y
+
 let compute_eqn env sigma n i ai =
   (mkRel (n-i),get_type_of env sigma (mkRel (n-i)))
 
@@ -94,7 +99,7 @@ let make_inv_predicate env evd indf realargs id status concl =
               | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*)
               | None ->
 		let sort = get_sort_family_of env !evd concl in
-                let sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd sort in
+                let sort = evd_comb1 Evd.fresh_sort_in_family evd sort in
 		let p = make_arity env !evd true indf sort in
 		let evd',(p,ptyp) = Unification.abstract_list_all env
                   !evd p concl (realargs@[mkVar id])
@@ -124,19 +129,19 @@ let make_inv_predicate env evd indf realargs id status concl =
 	      evd := sigma; res
 	in
         let eq_term = eqdata.Coqlib.eq in
-	let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in
+        let eq = evd_comb1 (Evd.fresh_global env) evd eq_term in
         let eqn = applist (eq,[eqnty;lhs;rhs]) in
         let eqns = (Anonymous, lift n eqn) :: eqns in
         let refl_term = eqdata.Coqlib.refl in
-	let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
+        let refl_term = evd_comb1 (Evd.fresh_global env) evd refl_term in
         let refl = mkApp (refl_term, [|eqnty; rhs|]) in
-	let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
+        let _ = evd_comb1 (Typing.type_of env) evd refl in
         let args = refl :: args in
         build_concl eqns args (succ n) restlist
   in
   let (newconcl, args) = build_concl [] [] 0 realargs in
   let predicate = it_mkLambda_or_LetIn newconcl (name_context env !evd hyps) in
-  let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
+  let _ = evd_comb1 (Typing.type_of env) evd predicate in
   (* OK - this predicate should now be usable by res_elimination_then to
      do elimination on the conclusion. *)
   predicate, args