coq-waterproof 2.2.0+8.17 · OCaml Package

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

val tclLOG : 
  (Environ.env -> Evd.evar_map -> Pp.t * Pp.t) ->
  Backtracking.trace Proofview.tactic ->
  Pp.t list ->
  Backtracking.trace Proofview.tactic

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

val trace_check_used : 
  Pp.t list ->
  Backtracking.trace ->
  Backtracking.trace Proofview.tactic

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

val tclOrElse0 : 
  Backtracking.trace Proofview.tactic ->
  (Backtracking.trace -> Backtracking.trace Proofview.tactic) ->
  Backtracking.trace Proofview.tactic

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

val tclTraceOrElse : 
  Backtracking.trace Proofview.tactic ->
  Backtracking.trace Proofview.tactic ->
  Backtracking.trace Proofview.tactic

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

val tclTraceFirst : 
  Backtracking.trace Proofview.tactic list ->
  Backtracking.trace Proofview.tactic

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

val pr_hint : Environ.env -> Evd.evar_map -> Hints.FullHint.t -> Pp.t

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

package coq-waterproof