From c6cabd1ff266a91022eb86caf4a99e89c0626430 Mon Sep 17 00:00:00 2001
From: Fabian Kunze
Date: Fri, 27 Nov 2020 11:11:23 +0100
Subject: Improved error message on nested proofs to include most common reason
 when this happens on accident

---
 stm/stm.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index f7d66b7b53..1c06c1efb7 100644
--- 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
-- 
cgit v1.2.3