Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative

3 files changed, 14 insertions, 0 deletions

diff --git a/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst
new file mode 100644
index 0000000000..ad7cf44482
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Added :flag:`Cumulative StrictProp` to control cumulativity of
+  |SProp| and deprecated now redundant command line
+  ``--cumulative-sprop`` (`#12034
+  <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 9acdd18b89..b2d3687780 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -240,3 +240,10 @@ so correctly converts ``x`` and ``y``.
   the kernel when it is passed a term with incorrect relevance marks.
   To avoid conversion issues as in ``late_mark`` you may wish to use
   it to find when your tactics are producing incorrect marks.
+
+.. flag:: Cumulative StrictProp
+   :name: Cumulative StrictProp
+
+   Set this flag (it is off by default) to make the kernel accept
+   cumulativity between |SProp| and other universes. This makes
+   typechecking incomplete.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7d031b9b7a..f9f7e70baa 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1076,6 +1076,8 @@ Controlling Typing Flags
    Print the status of the three typing flags: guard checking, positivity checking
    and universe checking.
 
+See also :flag:`Cumulative StrictProp` in the |SProp| chapter.
+
 .. example::
 
    .. coqtop:: all reset