aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_global.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_global.ml')
-rw-r--r--proofs/proof_global.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7605f6387..7b43b64ef 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -202,8 +202,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
+ "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