package coq-waterproof

  1. Overview
  2. Docs

Module Waterproof.ProofutilsSource

Sourceval find_first : ('a -> bool) -> 'a list -> int option

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

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

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

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

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

Sourcemodule StringMap : sig ... end

Generic dictionnary taking strings as keys

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

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

Sourcemodule type Mergeable = sig ... end

Generic mergeable type

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

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

Sourcemodule TraceTactics : sig ... end
Sourceval 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
Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

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

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