diff options
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. } *) |