Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative

3 files changed, 7 insertions, 5 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index cfc89782a1..17435c051e 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -44,7 +44,6 @@ type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
   toplevel_name     : Stm.interactive_top;
-  cumulative_sprop  : bool;
 }
 
 type coqargs_config = {
@@ -110,7 +109,6 @@ let default_logic_config = {
   impredicative_set = Declarations.PredicativeSet;
   indices_matter = false;
   toplevel_name = Stm.TopLogical default_toplevel;
-  cumulative_sprop = false;
 }
 
 let default_config = {
@@ -198,6 +196,10 @@ let set_query opts q =
   | Queries queries -> Queries (queries@[q])
   }
 
+let warn_deprecated_sprop_cumul =
+  CWarnings.create ~name:"deprecated-spropcumul" ~category:"deprecated"
+         (fun () -> Pp.strbrk "Use the \"Cumulative StrictProp\" flag instead.")
+
 let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
          (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.")
@@ -520,7 +522,9 @@ let parse_args ~help ~init arglist : t * string list =
       add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
     |"-disallow-sprop" ->
       add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
-    |"-sprop-cumulative" -> set_logic (fun o -> { o with cumulative_sprop = true }) oval
+    |"-sprop-cumulative" ->
+      warn_deprecated_sprop_cumul();
+      add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None)
     |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
     |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
     |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 8723d21bb4..a51ed6766a 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -20,7 +20,6 @@ type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
   toplevel_name     : Stm.interactive_top;
-  cumulative_sprop  : bool;
 }
 
 type coqargs_config = {
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1175494bad..7aad856d0a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -199,7 +199,6 @@ let init_execution opts custom_init =
   Global.set_VM opts.config.enable_VM;
   Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
   Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
-  if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative ();
 
   (* Native output dir *)
   Nativelib.output_dir := opts.config.native_output_dir;