From b1a9b3c33e91cffabc7ad68d7fdeadd18f384044 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 10 Apr 2019 09:25:51 +0200
Subject: Improve SProp error message to mention the Allow StrictProp flag.

And document the error message.
---
 doc/sphinx/addendum/sprop.rst | 3 +++
 vernac/himsg.ml               | 4 +++-
 2 files changed, 6 insertions(+), 1 deletion(-)

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)."
-- 
cgit v1.2.3