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/extraction/extraction.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ef6c07bff2..877ea9a537 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -73,13 +73,18 @@ type flag = info * scheme
 (*s [flag_of_type] transforms a type [t] into a [flag].
   Really important function. *)
 
+let info_of_family = function
+  | InSProp | InProp -> Logic
+  | InSet | InType -> Info
+
+let info_of_sort s = info_of_family (Sorts.family s)
+
 let rec flag_of_type env sg t : flag =
   let t = whd_all env sg t in
   match EConstr.kind sg t with
     | Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c
-    | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme)
-    | Sort _ -> (Info,TypeScheme)
-    | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default)
+    | Sort s -> (info_of_sort (EConstr.ESorts.kind sg s),TypeScheme)
+    | _ -> (info_of_family (sort_of env sg t),Default)
 
 (*s Two particular cases of [flag_of_type]. *)
 
-- 
cgit v1.2.3