diff options
| author | Emilio Jesus Gallego Arias | 2020-01-31 15:57:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-24 12:24:40 -0500 |
| commit | c216daf5d5f8215947bce10e55d30c35be1a56ba (patch) | |
| tree | d8b7eaf494bf01ee63d462d54ff85a67359f7c2a /user-contrib | |
| parent | 46fe9b26ad55a266b71bbd428ee406b03a9db030 (diff) | |
[exn] Forbid raising in exn printers, make them return Pp.t option
Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.
We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index d6db4a735c..a8bf4bc96f 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -848,8 +848,8 @@ let () = register_handler begin function let v = Tac2ffi.of_open (kn, args) in let t = GTypRef (Other t_exn, []) in let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in - hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c) -| _ -> raise Unhandled + Some (hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)) +| _ -> None end let () = CErrors.register_additional_error_info begin fun info -> |