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.
---
 dev/vm_printers.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/vm_printers.ml')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index dc30793a6e..863d930968 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -25,6 +25,7 @@ let print_vfix_app () = print_string "vfix_app"
 let print_vswith () = print_string "switch"
 
 let ppsort = function
+  | SProp -> print_string "SProp"
   | Set -> print_string "Set"
   | Prop -> print_string "Prop"
   | Type u -> print_string "Type"
-- 
cgit v1.2.3