Backport PR #13482: Improved error message on nested proofs

coq · Nov 28, 2020 · aadb979 · aadb979
2 parents 2b4a9d6 + 701e0ae
commit aadb979
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
@@ -173,7 +173,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       The name you provided is already defined. You have then to choose
       another name.
 
-   .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on.
+   .. exn:: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". \
+            If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on.
 
       You are asserting a new statement while already being in proof editing mode.
       This feature, called nested proofs, is disabled by default.

diff --git a/stm/stm.ml b/stm/stm.ml
@@ -2681,8 +2681,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
       | VtStartProof (guarantee, names) ->
 
          if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
-           "Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on."
-           |> Pp.str
+          "Nested proofs are discouraged and not allowed by default. \
+           This error probably means that you forgot to close the last \"Proof.\" with \"Qed.\" or \"Defined.\". \
+           If you really intended to use nested proofs, you can do so by turning the \"Nested Proofs Allowed\" flag on."
+           |> Pp.strbrk
            |> (fun s -> (UserError (None, s), Exninfo.null))
            |> State.exn_on ~valid:Stateid.dummy newtip
            |> Exninfo.iraise