[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.

6 files changed, 24 insertions, 12 deletions

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 1046fdc8d8..11e07175e3 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -258,8 +258,11 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 (** Evar combinators *)
 
 val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
+[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
 val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
+[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
 val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
+[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"]
 
 val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 839915631d..f7094ebe51 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -322,7 +322,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
   try
 
   let f = funs.(i) in
-  let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in
+  let sigma, type_sort = Evd.fresh_sort_in_family !evd InType in
+  evd := sigma;
   let new_sorts =
     match sorts with
       | None -> Array.make (Array.length funs) (type_sort)
@@ -507,8 +508,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
   let i = ref (-1) in
   let sorts =
     List.rev_map (fun (_,x) ->
-                  Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x
-             )
+        let sigma, fs = Evd.fresh_sort_in_family !evd x in
+        evd := sigma; fs
+      )
       fas
   in
   (* We create the first priciple by tactic *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2c821c96ba..9fa8442f8a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1713,7 +1713,8 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
       let vl = List.map pi1 good in
       let ty = 
         let ty = get_type_of !!env sigma t in
-          Evarutil.evd_comb1 (refresh_universes (Some false) !!env) evdref ty
+        let sigma, res = refresh_universes (Some false) !!env !evdref ty in
+        evdref := sigma; res
       in
       let dummy_subst = List.init k (fun _ -> mkProp) in
       let ty = substl dummy_subst (aux x ty) in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c0565f4f47..44bfe4b6cc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -46,7 +46,8 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   (* direction: true for fresh universes lower than the existing ones *)
   let refresh_sort status ~direction s =
     let s = ESorts.kind !evdref s in
-    let s' = evd_comb0 (new_sort_variable status) evdref in
+    let sigma, s' = new_sort_variable status !evdref in
+    evdref := sigma;
     let evd = 
       if direction then set_leq_sort env !evdref s' s
       else set_leq_sort env !evdref s s'
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 4ee7e667fe..e49ba75b3f 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -455,8 +455,8 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
       | ((indi,u),_,_,dep,kinds)::rest ->
 	  let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list mkRel i lnamesparrec) in
 	  let s = 
-            Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg)
-	      evdref kinds 
+            let sigma, res = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg !evdref kinds in
+            evdref := sigma; res
 	  in
 	  let typP = make_arity env !evdref dep indf s in
 	  let typP = EConstr.Unsafe.to_constr typP in
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