diff options
| author | Matthieu Sozeau | 2015-09-11 18:07:39 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:10 +0200 |
| commit | e759333a8b5c11247c4cc134fdde8c1bd85a6e17 (patch) | |
| tree | 8eb43cf88b6d2367bb856f46b2a471af583e73db /pretyping/evd.mli | |
| parent | 88abc50ece70405d71777d5350ca2fa70c1ff437 (diff) | |
Universes: enforce Set <= i for all Type occurrences.
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 94d9d5f662..c2ccc6d21a 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -505,9 +505,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is |