diff options
| author | Pierre-Marie Pédrot | 2020-02-03 09:18:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-03 09:18:41 +0100 |
| commit | 0ffd145a082f69aeb3980717f501d5c1c503a996 (patch) | |
| tree | 6e5cad60e5d7fa31b03d975f59367411bfd254b9 /vernac | |
| parent | e5da14f87fea2e99b5e4e70dc6340f40daaef41f (diff) | |
| parent | 173a2d8b0fba1a85b618654151af04b5decf9bac (diff) | |
Merge PR #11490: [exn] Don't reraise in exception printers
Ack-by: aspiwack
Reviewed-by: ppedrot
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacstate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index c81a4abc1b..80b72225f0 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -124,7 +124,7 @@ module Proof_global = struct let () = CErrors.register_handler begin function | NoCurrentProof -> - CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") + Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end |