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
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 conclPattern :
EConstr.constr ->
Pattern.constr_pattern option ->
Genarg.glob_generic_argument ->
unit Proofview.tactic
The Auto tactic
The use of the "core" database can be de-activated by passing "nocore" amongst the databases.
val auto :
?debug:Hints.debug ->
int ->
Tactypes.delayed_open_constr list ->
Hints.hint_db_name list ->
unit Proofview.tactic
Auto with more delta.
val default_auto : unit Proofview.tactic
auto with default search depth and with the hint database "core"
val full_auto :
?debug:Hints.debug ->
int ->
Tactypes.delayed_open_constr list ->
unit Proofview.tactic
auto with all hint databases
val default_full_auto : unit Proofview.tactic
auto with default search depth and with all hint databases
val gen_auto :
?debug:Hints.debug ->
int option ->
Tactypes.delayed_open_constr list ->
Hints.hint_db_name list option ->
unit Proofview.tactic
The generic form of auto (second arg None
means all bases)
val h_auto :
?debug:Hints.debug ->
int option ->
Tactypes.delayed_open_constr list ->
Hints.hint_db_name list option ->
unit Proofview.tactic
The hidden version of auto
Trivial
val trivial :
?debug:Hints.debug ->
Tactypes.delayed_open_constr list ->
Hints.hint_db_name list ->
unit Proofview.tactic
val gen_trivial :
?debug:Hints.debug ->
Tactypes.delayed_open_constr list ->
Hints.hint_db_name list option ->
unit Proofview.tactic
val full_trivial :
?debug:Hints.debug ->
Tactypes.delayed_open_constr list ->
unit Proofview.tactic
val h_trivial :
?debug:Hints.debug ->
Tactypes.delayed_open_constr list ->
Hints.hint_db_name list option ->
unit Proofview.tactic