diff options
| author | Maxime Dénès | 2018-03-08 21:22:59 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-08 21:22:59 +0100 |
| commit | a40fb961c8ffeeb03769404cacda8bd6cff17417 (patch) | |
| tree | 7105d621bc16f825c1f309e3d5b7720b1b1513ec /engine/evd.mli | |
| parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
| parent | 66973ce17e32a3c692a5b0032f38300ec8cc36d3 (diff) | |
Merge PR #6893: Cleanup UState API usage
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index ed3316c16d..49c953f6d3 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,22 +493,31 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t +[@@ocaml.deprecated "Alias of UState.context_set"] val evar_universe_context_constraints : UState.t -> Univ.Constraint.t +[@@ocaml.deprecated "Alias of UState.constraints"] val evar_context_universe_context : UState.t -> Univ.UContext.t [@@ocaml.deprecated "alias of UState.context"] val evar_universe_context_of : Univ.ContextSet.t -> UState.t +[@@ocaml.deprecated "Alias of UState.of_context_set"] val empty_evar_universe_context : UState.t +[@@ocaml.deprecated "Alias of UState.empty"] val union_evar_universe_context : UState.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.union"] val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +[@@ocaml.deprecated "Alias of UState.subst"] val constrain_variables : Univ.LSet.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.constrain_variables"] val evar_universe_context_of_binders : Universes.universe_binders -> UState.t +[@@ocaml.deprecated "Alias of UState.of_binders"] val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t +[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"] val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t @@ -516,13 +525,15 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t val universe_binders : evar_map -> Universes.universe_binders val add_constraints_context : UState.t -> Univ.Constraint.t -> UState.t +[@@ocaml.deprecated "Alias of UState.add_constraints"] val normalize_evar_universe_context_variables : UState.t -> Univ.universe_subst in_evar_universe_context +[@@ocaml.deprecated "Alias of UState.normalize_variables"] -val normalize_evar_universe_context : UState.t -> - UState.t +val normalize_evar_universe_context : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.minimize"] val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -581,12 +592,16 @@ val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_co val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"] val fix_undefined_variables : evar_map -> evar_map val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst +(** Universe minimization *) +val minimize_universes : evar_map -> evar_map val nf_constraints : evar_map -> evar_map +[@@ocaml.deprecated "Alias of Evd.minimize_universes"] val update_sigma_env : evar_map -> env -> evar_map |