diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 5c8b8944a73f..efd466b32426 100644
--- a/dev/doc/critical-bugs
+++ b/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
diff --git a/doc/changelog/01-kernel/14395-print-assum-section-flags.rst b/doc/changelog/01-kernel/14395-print-assum-section-flags.rst
new file mode 100644
index 000000000000..d9f90ad99224
--- /dev/null
+++ b/doc/changelog/01-kernel/14395-print-assum-section-flags.rst
@@ -0,0 +1,5 @@
+- **Changed:** Removed the ability to change typing flags inside
+  sections to prevent exploiting a weakness in :cmd:`Print
+  Assumptions` (`#14395 <https://github.com/coq/coq/pull/14395>`_,
+  fixes `#14317 <https://github.com/coq/coq/issues/14317>`_, by Gaëtan
+  Gilbert).
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 32957369b998..26fe84b8d2a6 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1017,6 +1017,7 @@ See also :flag:`Cumulative StrictProp` in the |SProp| chapter.
             end
           end.
 
+Typing flags may not be changed while inside sections.
 
 .. _internal-registration-commands:
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 414ef2b4d70d..1e1a3f5b03da 100644
--- a/kernel/environ.mli
+++ b/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
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5f83e78eb059..7e5aa6cb56e3 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -218,6 +218,18 @@ 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;
+             share_reduction = flags.share_reduction;
+            })
+  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
diff --git a/test-suite/output/bug_14317.v b/test-suite/bugs/closed/bug_14317.v
similarity index 64%
rename from test-suite/output/bug_14317.v
rename to test-suite/bugs/closed/bug_14317.v
index b579a53e9dbf..29601072ffef 100644
--- a/test-suite/output/bug_14317.v
+++ b/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 *)
diff --git a/test-suite/output/bug_14317.out b/test-suite/output/bug_14317.out
deleted file mode 100644
index dd3a9c728c3e..000000000000
--- a/test-suite/output/bug_14317.out
+++ /dev/null
@@ -1,2 +0,0 @@
-Axioms:
-loop is assumed to be guarded.