Auto (p.rocq-runtime.9.1.0.doc.rocq-runtime.tactics.Auto)

Sourceval compute_secvars : Proofview.Goal.t -> Names.Id.Pred.t

Sourceval default_search_depth : int

Default maximum search depth used by auto and trivial.

Sourceval auto_flags_of_state : TransparentState.t -> Unification.unify_flags

val unify_resolve : 
  Unification.unify_flags ->
  Hints.hint ->
  unit Proofview.tactic

Try unification with the precompiled clause, then use registered Apply

Source

val conclPattern : 
  EConstr.constr ->
  Pattern.constr_pattern option ->
  Gentactic.glob_generic_tactic ->
  unit Proofview.tactic

ConclPattern concl pat tacast: if the term concl matches the pattern pat, (in sense of Pattern.somatches, then replace ?1 ?2 metavars in tacast by the right values to build a tactic

Sourceval default_auto : unit Proofview.tactic

default_auto runs the tactic auto with:

Maximum search depth default_search_depth.
The hint database "core".
No additional lemma.

Source

val gen_auto : 
  ?debug:Hints.debug ->
  int option ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db_name list option ->
  unit Proofview.tactic

gen_auto ?debug depth lemmas hints runs the tactic auto.

debug controls whether to print a debug trace (Off by default). Off prints nothing, Info prints successful steps, and Debug prints all steps (including unsuccessful ones).
depth is the maximum search depth. If None, default_search_depth is used.
lemmas contains additional lemmas for auto to use.
hints is a list of hint databases to use. If None, _all_ existing hint databases are used. By default the "core" hint database is included: passing "nocore" will disable "core".

Source

val gen_trivial : 
  ?debug:Hints.debug ->
  Tactypes.delayed_open_constr list ->
  Hints.hint_db_name list option ->
  unit Proofview.tactic

gen_trivial runs the tactic trivial. See gen_auto for an explanation of the different options.