diff options
Diffstat (limited to 'proofs/proof_errors.ml')
| -rw-r--r-- | proofs/proof_errors.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/proofs/proof_errors.ml b/proofs/proof_errors.ml new file mode 100644 index 0000000000..e543b0c8fd --- /dev/null +++ b/proofs/proof_errors.ml @@ -0,0 +1,12 @@ +exception Exception of exn +exception Timeout +exception TacticFailure of exn + +let _ = Errors.register_handler begin function + | Timeout -> Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!") + | Exception e -> Errors.print e + | TacticFailure e -> Errors.print e + | _ -> Pervasives.raise Errors.Unhandled +end + + |