diff options
Diffstat (limited to 'proofs/proof_errors.mli')
| -rw-r--r-- | proofs/proof_errors.mli | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/proofs/proof_errors.mli b/proofs/proof_errors.mli deleted file mode 100644 index dd21d539c9..0000000000 --- a/proofs/proof_errors.mli +++ /dev/null @@ -1,18 +0,0 @@ -(** 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 |