Module `Waterproof.Proofutils`Source

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

Source

val 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

Source

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

Source

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

Source

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

Source

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

Source

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

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

package coq-waterproof

Module Waterproof.ProofutilsSource

Module `Waterproof.Proofutils`Source