diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-02 15:50:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-17 16:29:07 +0200 |
| commit | dbc820f0df53218e730eba34b44a3b1901f13b9e (patch) | |
| tree | 11720b5f35bbc51202eec80e27eca14e32f8064c /engine | |
| parent | 3e7863e9369d38537685576a8642dbe0c062d0c5 (diff) | |
Deprecate mixing univ minimization and evm normalization functions.
Normalization sounds like it should be semantically noop.
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 40c1ee082..8bb0d2f61 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -178,11 +178,14 @@ val nf_evar_map_undefined : evar_map -> evar_map val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] (** Normalize the evar map w.r.t. universes, after simplification of constraints. Return the substitution function for constrs as well. *) val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"] (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of Evar.t |