Class_tactics
This files implements typeclasses eauto
val set_typeclasses_strategy : search_strategy -> unit
val typeclasses_eauto :
?only_classes:bool ->
?best_effort:bool ->
?st:TransparentState.t ->
?strategy:search_strategy ->
depth:Int.t option ->
Hints.hint_db_name list ->
unit Proofview.tactic
val head_of_constr : Names.Id.t -> EConstr.constr -> unit Proofview.tactic
val not_evar : EConstr.constr -> unit Proofview.tactic
val is_ground : EConstr.constr -> unit Proofview.tactic
val autoapply : EConstr.constr -> Hints.hint_db_name -> unit Proofview.tactic
module Search : sig ... end