coq-waterproof 2.2.0+8.17 · OCaml Package

val feedback_log : Feedback.level -> Pp.t list Stdlib.ref

A rudimentary feedback log

val wp_feedback_logger_id : int option Stdlib.ref

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

val wp_feedback_logger : Feedback.feedback -> unit

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

val add_wp_feedback_logger : unit -> unit

Adds the wp_feedback_logger to Coq's feeedback mechanism

val print_hypothesis_help : bool Stdlib.ref

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

val last_thrown_warning : Pp.t option Stdlib.ref

The last thrown warning

val redirect_feedback : bool Stdlib.ref

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

val redirect_errors : bool Stdlib.ref

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

type 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

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 notice : Pp.t -> unit Proofview.tactic

Sends a notice

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

Send an info message

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

Throws an error

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

A general function for sending feedback

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

Check the last warning against a string

package coq-waterproof