diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-30 09:57:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-30 09:57:24 +0200 |
| commit | df9fe1be977c2c856b11a842233598f8a791db49 (patch) | |
| tree | a7f25d877acda30f02627f710002c682f61a39e1 /engine | |
| parent | c1e12fbc64c39739e4a9f7bbf92e42f1bcb6be24 (diff) | |
| parent | dbc820f0df53218e730eba34b44a3b1901f13b9e (diff) | |
Merge PR #6935: Separate universe minimization and evar normalization functions
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 d3937f28e..e3e8f16c8 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -186,11 +186,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 |