Auto
This files implements auto and related automation tactics
val compute_secvars : Proofview.Goal.t -> Names.Id.Pred.t
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
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
val default_auto : unit Proofview.tactic
default_auto
runs the tactic auto
with:
default_search_depth
."core"
.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.