package coq-waterproof

  1. Overview
  2. Docs
val find_first : ('a -> bool) -> 'a list -> int option

Returns the index of the first element x of l such that `f x` is true

val find_last : ('a -> bool) -> 'a list -> int option

Returns the index of the last element x of l such that `f x` is true

val tail_end : 'a list -> int -> 'a list

Returns the queue of the given list after the nth element included

module StringMap : sig ... end

Generic dictionnary taking strings as keys

val tclMAP_rev : ('a -> unit Proofview.tactic) -> 'a list -> unit Proofview.tactic

Maps the given function to the list then applies every returned tactic

module type Mergeable = sig ... end

Generic mergeable type

module TypedTactics (M : Mergeable) : sig ... end

Generalization of tactics defined in coq-core for Mergeable-typed tactics

module TraceTactics : sig ... end

Rewrite of Auto.tclLOG

Updates the trace contained in the given tactic.

Fails if the hint's name is forbidden, or if the proof will be complete without using all must-use lemmas.

Arguments:

  • pp: Environ.env -> Evd.evar_map -> Pp.t * Pp.t: function to obtain the printable version of (hint_name, source_hint_database)
  • tac: trace tactic: tactic that will be tried
  • must_use: : Pp.t list: list of tactics that must be used during the automation
  • forbidden: : Pp.t list: list of tactics that mustn't be used during the automation

Checks if every hint in must_use is contained in tac and returns an exception if not

Rewrite of Tacticals.tclORELSE0 to give the trace of the failed tactic instead of the exception

Wrapper around tclOrElse0 with merge of trace contained in the failed trace tactic into the second one

Rewrite of Tacticals.tclTraceFirst with trace tactic with a merge of traces of failed tactics

Rewrite of Coq's hint printer to keep only the necessary parts