diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-01 15:36:57 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:13 +0200 |
| commit | b3d97c2147418f44fc704807d3812b04921591af (patch) | |
| tree | 695491ad5693218e18e023ac36671c653cf15c71 /kernel/univ.mli | |
| parent | c1630c9dcdf91dc965b3c375d68e3338fb737531 (diff) | |
Univs: fix bug #4251, handling of template polymorphic constants.
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index ad33d597e..4cc8a2528 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -91,6 +91,9 @@ sig val is_level : t -> bool (** Test if the universe is a level or an algebraic universe. *) + val is_levels : t -> bool + (** Test if the universe is a lub of levels or contains +n's. *) + val level : t -> Level.t option (** Try to get a level out of a universe, returns [None] if it is an algebraic universe. *) |