diff options
| author | Pierre-Marie Pédrot | 2020-10-16 14:04:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-16 14:04:48 +0200 |
| commit | e583be62b74d71b5af159700e3a31f78fec9a7d2 (patch) | |
| tree | 3bf2e4c4a72e2bcae402ef20a950c286469c2b10 /plugins | |
| parent | 671262d6691897c70df68a88a8b37a895c0f976d (diff) | |
| parent | f24aa027fcba094e2cea08370c4a583e1c1da827 (diff) | |
Merge PR #13195: Add support for "typeclasses eauto bfs <int_or_var_opt>"
Reviewed-by: ppedrot
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 99fd6890e6..a86045b0a4 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 |