aboutsummaryrefslogtreecommitdiff
path: root/engine/logic_monad.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-02-25 10:26:02 +0100
committerPierre-Marie Pédrot2020-02-25 10:26:02 +0100
commitff3755c88f813f1a0e40e08128521cce81e38273 (patch)
tree7a43b69d3c3fd4dc66c79cd743858ac4bbcab1fc /engine/logic_monad.ml
parenta9deb354d00b9a402a63648d1cadf4c2c36bbdd1 (diff)
parent6e5f8099d1877197e6ecda3fd4edac8d48228661 (diff)
Merge PR #11498: [exn] Forbid raising in exn printers, make them return Pp.t option
Reviewed-by: ppedrot
Diffstat (limited to 'engine/logic_monad.ml')
-rw-r--r--engine/logic_monad.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 6df3378524..1caf2c2722 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -38,9 +38,9 @@ exception Tac_Timeout
exception TacticFailure of exn
let _ = CErrors.register_handler begin function
- | Exception e -> CErrors.print e
- | TacticFailure e -> CErrors.print e
- | _ -> raise CErrors.Unhandled
+ | Exception e -> Some (CErrors.print e)
+ | TacticFailure e -> Some (CErrors.print e)
+ | _ -> None
end
(** {6 Non-logical layer} *)