Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

4 files changed, 13 insertions, 0 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index bbccae8edb..d682d3641f 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -60,6 +60,8 @@ type t = {
   indices_matter : bool;
   enable_VM : bool;
   native_compiler : native_compiler;
+  allow_sprop : bool;
+  cumulative_sprop : bool;
 
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
@@ -110,6 +112,8 @@ let default = {
   indices_matter = false;
   enable_VM = true;
   native_compiler = default_native;
+  allow_sprop = false;
+  cumulative_sprop = false;
 
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
@@ -477,6 +481,9 @@ let parse_args ~help ~init arglist : t * string list =
     |"-filteropts" -> { oval with filter_opts = true }
     |"-impredicative-set" ->
       { oval with impredicative_set = Declarations.ImpredicativeSet }
+    |"-allow-sprop" -> { oval with allow_sprop = true }
+    |"-disallow-sprop" -> { oval with allow_sprop = false }
+    |"-sprop-cumulative" -> { oval with cumulative_sprop = true }
     |"-indices-matter" -> { oval with indices_matter = true }
     |"-m"|"--memory" -> { oval with memory_stat = true }
     |"-noinit"|"-nois" -> { oval with load_init = false }
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index b89a88d1f6..97a62e97e4 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -35,6 +35,8 @@ type t = {
   indices_matter : bool;
   enable_VM : bool;
   native_compiler : native_compiler;
+  allow_sprop : bool;
+  cumulative_sprop : bool;
 
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 92ac200bc0..f7fb26fe3a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -189,6 +189,8 @@ let init_toplevel ~help ~init custom_init arglist =
   Global.set_indices_matter opts.indices_matter;
   Global.set_VM opts.enable_VM;
   Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true);
+  Global.set_allow_sprop opts.allow_sprop;
+  if opts.cumulative_sprop then Global.make_sprop_cumulative ();
 
   (* Allow the user to load an arbitrary state here *)
   inputstate opts;
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 94ec6bb70d..513374c2af 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -69,6 +69,8 @@ let print_usage_common co command =
 \n  -noglob                do not dump globalizations\
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -impredicative-set     set sort Set impredicative\
+\n  -allow-sprop           allow using the proof irrelevant SProp sort\
+\n  -sprop-cumulative      make sort SProp cumulative with the rest of the hierarchy\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\
 \n  -mangle-names x        mangle auto-generated names using prefix x\