diff options
| author | Emilio Jesus Gallego Arias | 2018-09-18 15:22:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-06 14:32:23 +0200 |
| commit | 53870b7f6890a593d1da93706f3d020a79d226e5 (patch) | |
| tree | 0f6e1afa1ca58611e6a12596ef10c88359b8045e /engine/evarutil.mli | |
| parent | 371566f7619aed79aad55ffed6ee0920b961be6e (diff) | |
[api] Remove (most) 8.9 deprecated objects.
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 0ad323ac4b..1046fdc8d8 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -173,14 +173,6 @@ 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"] - -(** 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 val flush_and_check_evars : evar_map -> constr -> Constr.constr @@ -273,25 +265,3 @@ val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Lo Evar_kinds.t Loc.located val meta_counter_summary_tag : int Summary.Dyn.tag - -val e_new_evar : - env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> types -> constr -[@@ocaml.deprecated "Use [Evarutil.new_evar]"] - -val e_new_type_evar : env -> evar_map ref -> - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t -[@@ocaml.deprecated "Use [Evarutil.new_type_evar]"] - -val e_new_Type : ?rigid:rigid -> evar_map ref -> constr -[@@ocaml.deprecated "Use [Evarutil.new_Type]"] - -val e_new_global : evar_map ref -> GlobRef.t -> constr -[@@ocaml.deprecated "Use [Evarutil.new_global]"] - -val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst -[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] |