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

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8e49800982..d5cb25d1fb 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -755,6 +755,7 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
 (* mapping glob_constr to constr_expr                                    *)
 
 let extern_glob_sort = function
+  | GSProp -> GSProp
   | GProp -> GProp
   | GSet -> GSet
   | GType _ as s when !print_universes -> s
-- 
cgit v1.2.3