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 | |
| 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')
| -rw-r--r-- | doc/changelog/01-kernel/10811-sprop-default-on.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 7 |
2 files changed, 7 insertions, 3 deletions
diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst new file mode 100644 index 0000000000..349c44c205 --- /dev/null +++ b/doc/changelog/01-kernel/10811-sprop-default-on.rst @@ -0,0 +1,3 @@ +- Using ``SProp`` is now allowed by default, without needing to pass + ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 + <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert). 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: |