diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index e44e8e9069..020f0a7b44 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -439,6 +439,9 @@ val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option (** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is not a sort variable declared in [evm] *) +val is_flexible_level : evar_map -> Univ.Level.t -> bool + + val whd_sort_variable : evar_map -> constr -> constr (* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *) val normalize_universe : evar_map -> Univ.universe -> Univ.universe |