diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 35 |
1 files changed, 26 insertions, 9 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index b28ce2a62d..49c953f6d3 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -318,8 +320,8 @@ exception UniversesDiffer val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map (** Add the given universe unification constraints to the evar map. - @raises UniversesDiffer in case a first-order unification fails. - @raises UniverseInconsistency + @raise UniversesDiffer in case a first-order unification fails. + @raise UniverseInconsistency . *) (** {5 Extra data} @@ -491,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 -> (Id.t located) list option -> UState.t +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 @@ -514,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 @@ -579,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 |