diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-24 15:50:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-27 15:15:42 +0200 |
| commit | 051f2c1be929a46a0713b47b072bb5be0a7558d0 (patch) | |
| tree | 9071a28a89d83bb6cffb82d0a3a3716b10a00e4f | |
| parent | bc6de5aa4e00dfc19c4866de4876f6213546fa5c (diff) | |
Fast path when checking equality of universe levels in UState.
We export the relevant level equality function in UGraph which is way faster
than checking that each one is smaller than the other as universes.
| -rw-r--r-- | engine/uState.ml | 2 | ||||
| -rw-r--r-- | kernel/uGraph.mli | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 353d8976d..e27d0536d 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -148,7 +148,7 @@ let process_universe_constraints ctx cstrs = instantiate_variable l' r vars else if is_local r' then instantiate_variable r' l vars - else if not (UGraph.check_eq univs l r) then + else if not (UGraph.check_eq_level univs l' r') then (* Two rigid/global levels, none of them being local, one of them being Prop/Set, disallow *) if Univ.Level.is_small l' || Univ.Level.is_small r' then diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index e95cf4d1c..ed52832fa 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -17,6 +17,7 @@ type universes = t type 'a check_function = universes -> 'a -> 'a -> bool val check_leq : universe check_function val check_eq : universe check_function +val check_eq_level : universe_level check_function (** The empty graph of universes *) val empty_universes : universes |