Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

6 files changed, 42 insertions, 19 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index d47a93c70d..a16a871dc3 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,5 +1,6 @@
 Analyze
 
+CheckFlags
 CheckInductive
 Mod_checking
 CheckTypes
diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml
new file mode 100644
index 0000000000..1f5e76bd83
--- /dev/null
+++ b/checker/checkFlags.ml
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Declarations
+
+let set_local_flags flags env =
+  let flags =
+    { (Environ.typing_flags env) with
+      check_guarded = flags.check_guarded;
+      check_positive = flags.check_positive;
+      check_universes = flags.check_universes;
+      conv_oracle = flags.conv_oracle;
+      cumulative_sprop = flags.cumulative_sprop;
+    }
+  in
+  Environ.set_typing_flags flags env
diff --git a/checker/checkFlags.mli b/checker/checkFlags.mli
new file mode 100644
index 0000000000..2e41e656f1
--- /dev/null
+++ b/checker/checkFlags.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val set_local_flags : Declarations.typing_flags -> Environ.env -> Environ.env
+(** Set flags except for those ignored by the checker (eg vm_compute). *)
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index a1d5aedb01..c370a77ea0 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -164,16 +164,7 @@ let check_inductive env mind mb =
         mind_private; mind_typing_flags; }
     =
     (* Locally set typing flags for further typechecking *)
-    let mb_flags = mb.mind_typing_flags in
-    let env = Environ.set_typing_flags
-        {env.env_typing_flags with
-         check_guarded = mb_flags.check_guarded;
-         check_positive = mb_flags.check_positive;
-         check_universes = mb_flags.check_universes;
-         conv_oracle = mb_flags.conv_oracle;
-        }
-        env
-    in
+    let env = CheckFlags.set_local_flags mb.mind_typing_flags env in
     Indtypes.check_inductive env ~sec_univs:None mind entry
   in
   let check = check mind in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 44b7089fd0..8fd81d43be 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -17,14 +17,7 @@ let set_indirect_accessor f = indirect_accessor := f
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
-  let cb_flags = cb.const_typing_flags in
-  let env = Environ.set_typing_flags
-      {env.env_typing_flags with
-       check_guarded = cb_flags.check_guarded;
-       check_universes = cb_flags.check_universes;
-       conv_oracle = cb_flags.conv_oracle;}
-      env
-  in
+  let env = CheckFlags.set_local_flags cb.const_typing_flags env in
   let poly, env =
     match cb.const_universes with
     | Monomorphic ctx ->
diff --git a/checker/values.ml b/checker/values.ml
index b9efce6948..9bd381e4a9 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -241,7 +241,10 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
+  v_tuple "typing_flags"
+    [|v_bool; v_bool; v_bool;
+      v_oracle; v_bool; v_bool;
+      v_bool; v_bool; v_bool|]
 
 let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]