package coq-waterproof

  1. Overview
  2. Docs
type wexn =
  1. | CastError of string
    (*

    Indicates that a cast made by the FFI has failed

    *)
  2. | FailedAutomation of string
    (*

    Indicates that the automatic solver called has failed

    *)
  3. | FailedTest of string
    (*

    Indicates that the running test has failed

    *)
  4. | NonExistingDataset of Hints.hint_db_name
    (*

    Indicates that the user tried to import a non-existing hint dataset

    *)
  5. | UnusedLemmas
    (*

    Indicates that no proof using all the given lemmas has been found

    *)
  6. | ToUserError of Pp.t
    (*

    An error that should go directly to the user

    *)

Type of exceptions used in Wateproof

val throw : ?info:Exninfo.info -> wexn -> 'a

Throws an error with given info and message

val warn : Pp.t -> unit Proofview.tactic

Sends a warning

val err : Pp.t -> unit Proofview.tactic

Throws an error