diff options
| author | Pierre-Marie Pédrot | 2019-10-14 07:05:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-14 07:05:01 +0200 |
| commit | 54e31c28bf21caf7f8fcff1fcf4b415fed66dc3a (patch) | |
| tree | 038374a730db66e8a2284f7b186925a654a7369e /doc/sphinx | |
| parent | 7623da4448381955ef063dcce6f4263d91fe0d74 (diff) | |
| parent | 825d0737069debb8e16c44cd49ad3a273211f76c (diff) | |
Merge PR #10811: Allow SProp default on
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 7 |
1 files changed, 4 insertions, 3 deletions
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: |