diff options
| author | Matthieu Sozeau | 2013-11-04 18:19:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:55 +0200 |
| commit | ede4fa2f51bee0a425f68cd159178835a3af3ca6 (patch) | |
| tree | 0cbd06a11bdc25ef4b1d8e81af23f5b5f4cfe9cc /pretyping/evd.mli | |
| parent | 7dfb0fb915fa095f8af57e8bb5e4727ebb61304a (diff) | |
Restore reasonable performance by not allocating during universe checks,
using a fast_compare_neq.
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 |