diff options
Diffstat (limited to 'proofs/proof_errors.mli')
| -rw-r--r-- | proofs/proof_errors.mli | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/proofs/proof_errors.mli b/proofs/proof_errors.mli new file mode 100644 index 0000000000..dd21d539c9 --- /dev/null +++ b/proofs/proof_errors.mli @@ -0,0 +1,18 @@ +(** This small files declares the exceptions needed by Proofview_gen, + as Coq's extraction cannot produce exception declarations. *) + +(** To help distinguish between exceptions raised by the IO monad from + the one used natively by Coq, the former are wrapped in + [Exception]. It is only used internally so that [catch] blocks of + the IO monad would only catch exceptions raised by the [raise] + function of the IO monad, and not for instance, by system + interrupts. Also used in [Proofview] to avoid capturing exception + from the IO monad ([Proofview] catches errors in its compatibility + layer, and when lifting goal-level expressions). *) +exception Exception of exn +(** This exception is used to signal abortion in [timeout] functions. *) +exception Timeout +(** This exception is used by the tactics to signal failure by lack of + successes, rather than some other exceptions (like system + interrupts). *) +exception TacticFailure of exn |