Forbid changing typing flags inside sections

Fix coq#14317

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 *)