From bcc050beebe32a1d94844875cf1e8c752e4b3985 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 Feb 2015 10:08:57 +0100
Subject: Granting wish #4008.

---
 proofs/proof_global.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f55ab70073..9717292456 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -339,10 +339,13 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
 type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
 
 let return_proof () =
-  let { proof; strength = (_,poly,_) } = cur_pstate () in
+  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
   let initial_goals = Proof.initial_goals proof in
   let evd =
-    let error s = raise (Errors.UserError("last tactic before Qed",s)) in
+    let error s =
+      let prf = str " (in proof " ++ Id.print pid ++ str ")" in
+      raise (Errors.UserError("last tactic before Qed",s ++ prf))
+    in
     try Proof.return proof with
     | Proof.UnfinishedProof ->
         error(str"Attempt to save an incomplete proof")
-- 
cgit v1.2.3