Checker: factorize handling of typing flags

5 files changed, 37 insertions, 18 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..e8c7dfdfeb
--- /dev/null
+++ b/checker/checkFlags.ml
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*         *   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;
+    }
+  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 ->