From 75508769762372043387c67a9abe94e8f940e80a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 27 Oct 2017 14:03:51 +0200
Subject: Add a non-cumulative impredicative universe SProp.

Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
---
 kernel/uGraph.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index e1a5d50425..17d6c6e6d3 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -13,6 +13,9 @@ open Univ
 (** {6 Graphs of universes. } *)
 type t
 
+val make_sprop_cumulative : t -> t
+(** Don't use this in the kernel, it makes the system incomplete. *)
+
 type 'a check_function = t -> 'a -> 'a -> bool
 
 val check_leq : Universe.t check_function
-- 
cgit v1.2.3