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.
---
 engine/evarutil.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine')

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