diff options
| author | Pierre-Marie Pédrot | 2020-02-25 10:26:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-25 10:26:02 +0100 |
| commit | ff3755c88f813f1a0e40e08128521cce81e38273 (patch) | |
| tree | 7a43b69d3c3fd4dc66c79cd743858ac4bbcab1fc /user-contrib | |
| parent | a9deb354d00b9a402a63648d1cadf4c2c36bbdd1 (diff) | |
| parent | 6e5f8099d1877197e6ecda3fd4edac8d48228661 (diff) | |
Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t option
Reviewed-by: ppedrot
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 70cba858c9..2a0c109a42 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 -> |