diff options
| author | Gaëtan Gilbert | 2017-09-15 22:21:46 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-24 19:18:56 +0100 |
| commit | 60770e86f4ec925fce52ad3565a92beb98d253c1 (patch) | |
| tree | 427bc507cffa5848bead327b04547154c8d23591 /engine/evd.mli | |
| parent | a5feb9687819c5e7ef0db6e7b74d0e236a296674 (diff) | |
Stop exposing UState.universe_context and its Evd wrapper.
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index b6157202de..49b6a75833 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -492,6 +492,8 @@ type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t val evar_universe_context_constraints : UState.t -> Univ.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 val empty_evar_universe_context : UState.t val union_evar_universe_context : UState.t -> UState.t -> @@ -552,11 +554,14 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t -val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> - Univ.UContext.t val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t +(** [to_universe_context evm] extracts the local universes and + constraints of [evm] and orders the universes the same as + [Univ.ContextSet.to_context]. *) +val to_universe_context : evar_map -> Univ.UContext.t + val check_univ_decl : evar_map -> UState.universe_decl -> Univ.UContext.t |