diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-11-14 11:50:04 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:55 +0200 |
| commit | c1cd47d5dff18f12af063d2c8defbd985c97dec6 (patch) | |
| tree | e459818ae127339883bb124a525191215a3b38f2 /checker/check.mllib | |
| parent | 28e5f4def8bebdaf3bd75b6662bbd4fd88594689 (diff) | |
- Fix comparison of universes.
- Shortcut for Set <= x checks, assuming that this is always true except when
x (or rather its canonical representative) is Prop. Invariant to check.
- Uncomment the profiling code and make it depend on a (statically known) boolean.
Diffstat (limited to 'checker/check.mllib')
| -rw-r--r-- | checker/check.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 12cfe4a48..7488a2c57 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -30,6 +30,7 @@ Ephemeron Future CUnix System +Profile RemoteCounter Envars Predicate |