From e841deb4750d43ab19f91907476d75fc73860c5a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:09:14 +0200 Subject: 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. --- kernel/univ.mli | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'kernel/univ.mli') 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. } *) -- cgit v1.2.3