diff options
| author | Jim Fehrle | 2020-10-14 23:40:17 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-14 23:40:17 -0700 |
| commit | f24aa027fcba094e2cea08370c4a583e1c1da827 (patch) | |
| tree | 4da25c70621b8b008883c78acbe278107bc007d8 /plugins | |
| parent | 411025844a4c005ce03d77c6c640807c28269d4a (diff) | |
Add support for "typeclasses eauto bfs <int_or_var_opt>
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_class.mlg | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 8d197e6056..0dd8939211 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -87,11 +87,13 @@ END (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - { typeclasses_eauto ~strategy:Bfs ~depth:d l } + { typeclasses_eauto ~depth:d ~strategy:Bfs l } | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> { typeclasses_eauto ~depth:d l } + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> { + typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] } | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { - typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] } + typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] } END TACTIC EXTEND head_of_constr |