Module Auto

This files implements auto and related automation tactics

val compute_secvars : Proofview.Goal.t -> Names.Id.Pred.t
val default_search_depth : int

Default maximum search depth used by auto and trivial.

val 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

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

val 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.
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".
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.