From 3231196c77c0641d7c59191bf691378b334afc46 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 6 Apr 2020 14:41:45 +0200
Subject: Make cumulative sprop a typing flag, deprecate command line
 -sprop-cumulative

---
 doc/sphinx/addendum/sprop.rst                   | 7 +++++++
 doc/sphinx/proof-engine/vernacular-commands.rst | 2 ++
 2 files changed, 9 insertions(+)

(limited to 'doc/sphinx')

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
-- 
cgit v1.2.3