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/proof-engine/vernacular-commands.rst | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/sphinx/proof-engine')

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