From dac8b249e95d376de587d7b527fd17f70e4942fc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 4 Oct 2018 23:21:57 +0200
Subject: [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.
---
 plugins/funind/functional_principles_types.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'plugins')

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