diff options
| author | Théo Zimmermann | 2020-04-26 22:27:42 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-27 12:12:57 +0200 |
| commit | 7f9e6dfcb5f78e60236a5d9359ef8b94792fddef (patch) | |
| tree | 3c944fd9fdfe68462b592c6e4f5a2b7475982cf6 | |
| parent | 85d77281bb69e9b0ec802f3955cc732c7bb0d5d3 (diff) | |
Improve the Allow SProp error message.
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 18 | ||||
| -rw-r--r-- | vernac/himsg.ml | 6 |
2 files changed, 10 insertions, 14 deletions
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index b2d3687780..c1b793b03e 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -12,22 +12,18 @@ proof irrelevant propositions (types in the sort :math:`\SProp`, also known as strict propositions) as described in :cite:`Gilbert:POPL2019`. -Using :math:`\SProp` may be prevented by passing ``-disallow-sprop`` -to the |Coq| program or using :flag:`Allow StrictProp`. +Use of |SProp| may be disabled by passing ``-disallow-sprop`` to the +|Coq| program or by turning the :flag:`Allow StrictProp` flag off. .. 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 - ``-disallow-sprop`` and ``-allow-sprop``. + Enables or disables the use of |SProp|. It is enabled by default. + The command-line flag ``-disallow-sprop`` disables |SProp| at + startup. -.. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag. - :undocumented: - -.. coqtop:: none - - Set Allow StrictProp. + .. exn:: SProp is disallowed because the "Allow StrictProp" flag is off. + :undocumented: Some of the definitions described in this document are available through ``Coq.Logic.StrictProp``, which see. diff --git a/vernac/himsg.ml b/vernac/himsg.ml index fddc84b398..41f2ab9c63 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -729,9 +729,9 @@ let explain_undeclared_universe env sigma l = spc () ++ str "(maybe a bugged tactic)." let explain_disallowed_sprop () = - Pp.(strbrk "SProp not allowed, you need to " - ++ str "Set Allow StrictProp" - ++ strbrk " or to use the -allow-sprop command-line-flag.") + Pp.(strbrk "SProp is disallowed because the " + ++ str "\"Allow StrictProp\"" + ++ strbrk " flag is off.") let explain_bad_relevance env = strbrk "Bad relevance (maybe a bugged tactic)." |