diff options
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 -> |