Forbid changing typing flags inside sections

Fix coq#14317

dev/doc/critical-bugs

@@ -366,6 +366,18 @@ Side-effects
   GH issue number: #13330
   risk: unlikely to be exploited by mistake, requires the use of unsafe tactics
 
+Forgetting unsafe flags
+
+  component: sections
+  summary: unsafe typing flags used inside a section would not be reported by Print Assumptions
+           after closing the section
+  introduced: abab878b8d8b5ca85a4da688abed68518f0b17bd (#10291, 8.11)
+              technically available earlier through plugins
+  impacted coqchk versions: none (coqchk rejects affected files)
+  found by: Anton Trunov
+  GH issue number: #14317
+  risk: low as it needs the use of explicit unsafe flags 
+
 Conflicts with axioms in library
 
   component: library of real numbers

kernel/environ.mli

@@ -356,6 +356,8 @@ val set_type_in_type : bool -> env -> env
 val set_allow_sprop : bool -> env -> env
 val sprop_allowed : env -> bool
 
+val same_flags : typing_flags -> typing_flags -> bool
+
 (** [update_typing_flags ?typing_flags] may update env with optional typing flags *)
 val update_typing_flags : ?typing_flags:typing_flags -> env -> env
 

kernel/safe_typing.ml

@@ -218,6 +218,15 @@ let set_typing_flags c senv =
   if env == senv.env then senv
   else { senv with env }
 
+let set_typing_flags flags senv =
+  (* NB: we allow changing the conv_oracle inside sections because it
+     doesn't matter for consistency. *)
+  if Option.has_some senv.sections
+  && not (Environ.same_flags flags
+            {(Environ.typing_flags senv.env) with conv_oracle = flags.conv_oracle})
+  then CErrors.user_err Pp.(str "Changing typing flags inside sections is not allowed.");
+  set_typing_flags flags senv
+
 let set_check_guarded b senv =
   let flags = Environ.typing_flags senv.env in
   set_typing_flags { flags with check_guarded = b } senv

test-suite/output/bug_14317.v → test-suite/bugs/closed/bug_14317.v

@@ -1,15 +1,15 @@
 Section FooSect.
 
-  Unset Guard Checking.
+  Fail Unset Guard Checking.
 
   (* Let bad := fix bad (n:nat) : False := bad n. *)
 
-  Fixpoint loop (n : nat) : nat := loop n.
+  (* Fixpoint loop (n : nat) : nat := loop n. *)
 
   (* Set Guard Checking. *)
   (* Definition really_bad := bad 0. *)
 
 End FooSect.
 
-Print Assumptions loop.
+(* Print Assumptions loop. *)
 (* Print Assumptions really_bad. TODO *)