diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-23 16:09:14 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:10 +0200 |
| commit | e841deb4750d43ab19f91907476d75fc73860c5a (patch) | |
| tree | b92b71db1d0a33864f8a0a1aa72f247a2f91b88a /kernel/univ.mli | |
| parent | cc69a4697633e14fc00c9bd0858b38120645464b (diff) | |
Univs (kernel) adapt to new invariants
Remove predicative flag and adapt to new invariant where every universe
must be declared, ensuring it is >= Set, safe_repr is not necessary
anymore.
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index fe7fc1ab9..ad33d597e 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -163,7 +163,11 @@ val is_initial_universes : universes -> bool val sort_universes : universes -> universes -(** Adds a universe to the graph, ensuring it is >= or > Set. *) +(** Adds a universe to the graph, ensuring it is >= or > Set. + @raises AlreadyDeclared if the level is already declared in the graph. *) + +exception AlreadyDeclared + val add_universe : universe_level -> bool -> universes -> universes (** {6 Constraints. } *) |