diff options
Diffstat (limited to 'tactics/g_class.ml4')
| -rw-r--r-- | tactics/g_class.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index 970f635b7..c7867a83c 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -63,8 +63,8 @@ VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF END TACTIC EXTEND typeclasses_eauto -| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ] -| [ "typeclasses" "eauto" ] -> [ typeclasses_eauto ~only_classes:true [Auto.typeclasses_db] ] +| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ Proofview.V82.tactic (typeclasses_eauto l) ] +| [ "typeclasses" "eauto" ] -> [ Proofview.V82.tactic (typeclasses_eauto ~only_classes:true [Auto.typeclasses_db]) ] END TACTIC EXTEND head_of_constr @@ -76,9 +76,9 @@ TACTIC EXTEND not_evar END TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ is_ground ty ] + [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ] END TACTIC EXTEND autoapply - [ "autoapply" constr(c) "using" preident(i) ] -> [ autoapply c i ] + [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply c i) ] END |