aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/Init.v
blob: b5352e720a29f5d81a7a3006b079d74e83e0d9b0 (plain)
1
Ltac typeclass_instantiation := eauto 50 with typeclass_instances || eauto.