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 From 825d0737069debb8e16c44cd49ad3a273211f76c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 5 Oct 2019 11:37:27 +0200 Subject: Changelog for SProp on --- doc/changelog/01-kernel/10811-sprop-default-on.rst | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 doc/changelog/01-kernel/10811-sprop-default-on.rst (limited to 'doc') 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 + `_, by Gaëtan Gilbert). -- cgit v1.2.3