diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-11-04 18:19:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:55 +0200 |
| commit | ede4fa2f51bee0a425f68cd159178835a3af3ca6 (patch) | |
| tree | 0cbd06a11bdc25ef4b1d8e81af23f5b5f4cfe9cc /pretyping/evd.ml | |
| parent | 7dfb0fb915fa095f8af57e8bb5e4727ebb61304a (diff) | |
Restore reasonable performance by not allocating during universe checks,
using a fast_compare_neq.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ef93a827a..21a0603c3 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1021,6 +1021,9 @@ let is_sort_variable evd s = | None -> None) | _ -> None +let is_flexible_level evd l = + let uctx = evd.universes in + Univ.LMap.mem l uctx.uctx_univ_variables let is_eq_sort s1 s2 = if Sorts.equal s1 s2 then None |