diff options
| -rw-r--r-- | proofs/proof_global.ml | 7 |
1 files 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") |