diff options
| author | Emilio Jesus Gallego Arias | 2020-01-30 23:36:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-01-30 23:36:19 +0100 |
| commit | 173a2d8b0fba1a85b618654151af04b5decf9bac (patch) | |
| tree | 8f7385dbc348bed11568414729ec4e1f65a295e4 /vernac | |
| parent | 869f731439b7fe034067bb550b60713b9b790f5b (diff) | |
[exn] Don't reraise in exception printers
This behaviour seems a bit dubious and it is indeed not needed, also
such re-raises seem like they will mess with the backtrace.
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 |