diff options
| author | Emilio Jesus Gallego Arias | 2018-10-04 23:21:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-07 19:41:45 +0200 |
| commit | dac8b249e95d376de587d7b527fd17f70e4942fc (patch) | |
| tree | 74be87f519c5fbd4c5f35355749f7050a2cb1da0 /engine/evarutil.mli | |
| parent | 9a13a86115823a24738489f0b11b692f4ed065ad (diff) | |
[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.
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 3 |
1 files changed, 3 insertions, 0 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 |