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

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

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

Generic dictionnary taking strings as keys

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

Generic mergeable type

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

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