diff options
| author | Gaëtan Gilbert | 2019-10-02 14:59:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-04 14:07:15 +0200 |
| commit | d7f43705e347f728d99e45720d8f2e0a3f7cff34 (patch) | |
| tree | 91c5ebaa86c5caab9171c2815dcdde5ea998f10a /doc | |
| parent | 87c17a6871ef4c21ff86a050297d33738c5a870a (diff) | |
Allow SProp default on
Diffstat (limited to 'doc')
| -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: |