From 7f9e6dfcb5f78e60236a5d9359ef8b94792fddef Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 26 Apr 2020 22:27:42 +0200
Subject: Improve the Allow SProp error message.

---
 vernac/himsg.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

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