diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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)." |