diff options
| author | Matthieu Sozeau | 2015-09-14 18:35:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-09-14 18:41:09 +0200 |
| commit | 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b (patch) | |
| tree | ce5b0fed1af0fb238a23d6b78a57a9bf2df29bb7 /pretyping/evd.mli | |
| parent | 490160d25d3caac1d2ea5beebbbebc959b1b3832 (diff) | |
Univs: Add universe binding lists to definitions
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index f2d8a83350..94d9d5f662 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -129,10 +129,13 @@ type evar_map val empty : evar_map (** The empty evar map. *) -val from_env : ?ctx:evar_universe_context -> env -> evar_map +val from_env : env -> evar_map (** The empty evar map with given universe context, taking its initial universes from env. *) +val from_ctx : evar_universe_context -> evar_map +(** The empty evar map with given universe context *) + val is_empty : evar_map -> bool (** Whether an evarmap is empty. *) @@ -484,6 +487,8 @@ val union_evar_universe_context : evar_universe_context -> evar_universe_context evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst +val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context +val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> string -> Univ.universe_level val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map @@ -527,7 +532,7 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : evar_map -> Univ.universe_context +val universe_context : ?names:(Id.t located) list -> evar_map -> Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> Univ.universes |