Module `Waterproof.Exceptions`Source

Sourceval feedback_log : Feedback.level -> Pp.t list ref

A rudimentary feedback log

Sourceval wp_feedback_logger_id : int option ref

The id that we obtained when registering wp_feedback_logger as a feeder in Feedback.mli

Sourceval wp_feedback_logger : Feedback.feedback -> unit

Our own logger that we add as a feeder to Coq's feedback mechanism in Feedback.mli

Sourceval add_wp_feedback_logger : unit -> unit

Adds the wp_feedback_logger to Coq's feeedback mechanism

Sourceval print_hypothesis_help : bool ref

Should hypothesis hints be printed (For instance on how you can use a forall statement)?

Sourceval last_thrown_warning : Pp.t option ref

The last thrown warning

Sourceval redirect_feedback : bool ref

Redirect warnings: this is useful when testing the plugin: meant to redirect Waterproof errors directly to the log

Sourceval redirect_errors : bool ref

Redirect errors: this is useful when testing the plugin: meant to redirect errors to Control.zero rather than CErrors.user_err

Sourcetype wexn =

| CastError of string
(*
Indicates that a cast made by the FFI has failed
*)
| FailedAutomation of string
(*
Indicates that the automatic solver called has failed
*)
| FailedTest of string
(*
Indicates that the running test has failed
*)
| NonExistingDataset of Hints.hint_db_name
(*
Indicates that the user tried to import a non-existing hint dataset
*)
| UnusedLemmas
(*
Indicates that no proof using all the given lemmas has been found
*)
| ToUserError of Pp.t
(*
An error that should go directly to the user
*)

Type of exceptions used in Wateproof

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

Throws an error with given info and message

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

Sends a warning

Sourceval notice : Pp.t -> unit Proofview.tactic

Sends a notice

Sourceval inform : Pp.t -> unit Proofview.tactic

Send an info message

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

Throws an error

Sourceval message : Feedback.level -> Pp.t -> unit Proofview.tactic

A general function for sending feedback

Sourceval get_last_warning : unit -> Pp.t option Proofview.tactic

Check the last warning against a string

package coq-waterproof