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.
---
 plugins/ltac/taccoerce.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 026c00b849..fcab98c7e8 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -199,7 +199,8 @@ let id_of_name = function
 	  basename
        | Sort s ->
           begin
-	    match ESorts.kind sigma s with
+            match ESorts.kind sigma s with
+            | Sorts.SProp -> Label.to_id (Label.make "SProp")
             | Sorts.Prop -> Label.to_id (Label.make "Prop")
             | Sorts.Set -> Label.to_id (Label.make "Set")
             | Sorts.Type _ -> Label.to_id (Label.make "Type")
-- 
cgit v1.2.3