blob: dd21d539c98918865ee6f137dcdef1bb4ba8d022 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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
|
