diff options
| author | Gaëtan Gilbert | 2019-04-10 12:52:02 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-04-10 12:52:02 +0200 |
| commit | dcf6560f00fde4a2564ba8489cdd34e7bdea5cfa (patch) | |
| tree | 74e4a4c1cfda4766435db187a9ae52f97b540bd1 | |
| parent | e3e3e6949f1c80abec9942ee0d258b58e5a7d382 (diff) | |
| parent | b1a9b3c33e91cffabc7ad68d7fdeadd18f384044 (diff) | |
Merge PR #9941: Improve SProp error message to mention the Allow StrictProp flag.
Reviewed-by: SkySkimmer
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 3 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 |
2 files changed, 6 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 015b84c530..c0c8c2d79c 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -19,6 +19,9 @@ known as strict propositions). To use :math:`\SProp` you must pass initial value depends on whether you used the command line ``-allow-sprop``. +.. 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. diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 32754478a5..d329b81341 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -731,7 +731,9 @@ let explain_undeclared_universe env sigma l = spc () ++ str "(maybe a bugged tactic)." let explain_disallowed_sprop () = - Pp.(str "SProp not allowed, you need to use -allow-sprop.") + Pp.(strbrk "SProp not allowed, you need to " + ++ str "Set Allow StrictProp" + ++ strbrk " or to use the -allow-sprop command-line-flag.") let explain_bad_relevance env = strbrk "Bad relevance (maybe a bugged tactic)." |