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.

1 files changed, 2 insertions, 0 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a3d2f33216..5ece892aa2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -306,6 +306,7 @@ let constr_display csr =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ())
 
   and sort_display = function
+    | SProp -> "SProp"
     | Set -> "Set"
     | Prop -> "Prop"
     | Type u -> univ_display u;
@@ -430,6 +431,7 @@ let print_pure_constr csr =
     Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u)
 
   and sort_display = function
+    | SProp -> print_string "SProp"
     | Set -> print_string "Set"
     | Prop -> print_string "Prop"
     | Type u -> open_hbox();