diff options
| author | Matthieu Sozeau | 2015-10-28 12:36:20 -0400 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-28 12:42:00 -0400 |
| commit | 0132b5b51fc1856356fb74130d3dea7fd378f76c (patch) | |
| tree | da5c0ec53dcecafb2fab5db1a112fac8b6311e60 /pretyping/evd.mli | |
| parent | 89be9efbf6dbd8a04fb8ccab4c9aa7a11b9a0f03 (diff) | |
Univs: local names handling.
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 9379b50b52..3c16b27ad9 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -487,6 +487,9 @@ 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 evar_universe_context_of_binders : + Universes.universe_binders -> evar_universe_context + 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. *) @@ -534,7 +537,8 @@ 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 : ?names:(Id.t located) list -> evar_map -> Univ.universe_context +val universe_context : ?names:(Id.t located) list -> evar_map -> + (Id.t * Univ.Level.t) list * Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> Univ.universes |