diff options
| author | Pierre-Marie Pédrot | 2018-10-08 10:15:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-08 10:15:12 +0200 |
| commit | 07ba57a0c313a86f4e0f87352cfa50646d00709f (patch) | |
| tree | 74be87f519c5fbd4c5f35355749f7050a2cb1da0 /engine | |
| parent | 9a13a86115823a24738489f0b11b692f4ed065ad (diff) | |
| parent | dac8b249e95d376de587d7b527fd17f70e4942fc (diff) | |
Merge PR #8582: [api] Deprecate `evar_map` ref combinators.
Diffstat (limited to 'engine')
| -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 |