aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_global.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-08 14:56:33 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-08 15:41:16 +0200
commit13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch)
treef76fd37023c71c20520e34e4a51c487e7a0388a0 /proofs/proof_global.ml
parent79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff)
parentfc579fdc83b751a44a18d2373e86ab38806e7306 (diff)
Merge PR #244.
Diffstat (limited to 'proofs/proof_global.ml')
-rw-r--r--proofs/proof_global.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 17cc92803..f3ca19a90 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -204,8 +204,8 @@ let discard (loc,id) =
let n = List.length !pstates in
discard_gen id;
if Int.equal (List.length !pstates) n then
- CErrors.user_err_loc
- (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
+ CErrors.user_err ~loc
+ ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
let discard_current () =
if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
@@ -410,7 +410,7 @@ let return_proof ?(allow_partial=false) () =
let evd =
let error s =
let prf = str " (in proof " ++ Id.print pid ++ str ")" in
- raise (CErrors.UserError("last tactic before Qed",s ++ prf))
+ raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf))
in
try Proof.return proof with
| Proof.UnfinishedProof ->
@@ -521,7 +521,7 @@ module Bullet = struct
(function
| FailedBullet (b,sugg) ->
let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
- CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
+ CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
| _ -> raise CErrors.Unhandled)