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.

1 files changed, 11 insertions, 4 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 77d1896683..6f4f40e2c5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -37,18 +37,25 @@ type t =
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
    uctx_weak_constraints : UPairSet.t
  }
-  
+
+let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes
+
 let empty =
   { uctx_names = UNameMap.empty, LMap.empty;
     uctx_local = ContextSet.empty;
     uctx_seff_univs = LSet.empty;
     uctx_univ_variables = LMap.empty;
     uctx_univ_algebraic = LSet.empty;
-    uctx_universes = UGraph.initial_universes;
-    uctx_initial_universes = UGraph.initial_universes;
+    uctx_universes = initial_sprop_cumulative;
+    uctx_initial_universes = initial_sprop_cumulative;
     uctx_weak_constraints = UPairSet.empty; }
 
+let elaboration_sprop_cumul =
+  Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
+    ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
+
 let make u =
+  let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in
     { empty with 
       uctx_universes = u; uctx_initial_universes = u}
 
@@ -710,7 +717,7 @@ let universe_of_name uctx s =
   UNameMap.find s (fst uctx.uctx_names)
 
 let update_sigma_env uctx env =
-  let univs = Environ.universes env in
+  let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
   let eunivs =
     { uctx with uctx_initial_universes = univs;
                          uctx_universes = univs }