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.
---
 printing/ppconstr.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 26202ef4ca..ad2b51b23d 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -169,12 +169,14 @@ let tag_var = tag Tag.variable
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
   let pr_glob_sort = let open Glob_term in function
+    | GSProp -> tag_type (str "SProp")
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
     | GType [] -> tag_type (str "Type")
     | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
 
   let pr_glob_level = let open Glob_term in function
+    | GSProp -> tag_type (str "SProp")
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
     | GType UUnknown -> tag_type (str "Type")
@@ -197,6 +199,8 @@ let tag_var = tag Tag.variable
   let pr_patvar = pr_id
 
   let pr_glob_sort_instance = let open Glob_term in function
+    | GSProp ->
+      tag_type (str "SProp")
     | GProp ->
       tag_type (str "Prop")
     | GSet ->
-- 
cgit v1.2.3