diff options
Diffstat (limited to 'plugins/ltac/g_class.mlg')
| -rw-r--r-- | plugins/ltac/g_class.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 8c2e633be5..0f59ac07b4 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -86,13 +86,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" "bfs" nat_or_var_opt(d) "with" ne_preident_list(l) ] -> { typeclasses_eauto ~depth:d ~strategy:Bfs l } - | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> + | [ "typeclasses" "eauto" nat_or_var_opt(d) "with" ne_preident_list(l) ] -> { typeclasses_eauto ~depth:d l } - | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> { + | [ "typeclasses" "eauto" "bfs" nat_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" nat_or_var_opt(d) ] -> { typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] } END |