From d7f43705e347f728d99e45720d8f2e0a3f7cff34 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 2 Oct 2019 14:59:03 +0200
Subject: Allow SProp default on

---
 doc/sphinx/addendum/sprop.rst | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 8935ba27e3..9a9ec78edc 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -9,15 +9,16 @@ SProp (proof irrelevant propositions)
 
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
-known as strict propositions). To use :math:`\SProp` you must pass
-``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`.
+known as strict propositions). Using :math:`\SProp` may be prevented
+by passing ``-disallow-sprop`` to the |Coq| program or using
+:flag:`Allow StrictProp`.
 
 .. flag:: Allow StrictProp
    :name: Allow StrictProp
 
    Allows using :math:`\SProp` when set and forbids it when unset. The
    initial value depends on whether you used the command line
-   ``-allow-sprop``.
+   ``-disallow-sprop`` and ``-allow-sprop``.
 
 .. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag.
    :undocumented:
-- 
cgit v1.2.3