bteauto: a Proofview.tactic for multiple goals

Add an option to force backtracking at toplevel, which
is used by default when calling typeclasses eauto on a set of goals.
They might be depended on by other subgoals, so the tactic should
be backtracking by default, a once can make it not backtrack.

1 files changed, 6 insertions, 5 deletions

diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 93fa3abd1..01af90e27 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -66,8 +66,9 @@ VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
 END
 
 TACTIC EXTEND typeclasses_eauto
-| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ Proofview.V82.tactic (typeclasses_eauto l) ]
-| [ "typeclasses" "eauto" ] -> [ Proofview.V82.tactic (typeclasses_eauto ~only_classes:true [Hints.typeclasses_db]) ]
+| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ]
+| [ "typeclasses" "eauto" ] -> [
+    typeclasses_eauto ~only_classes:true [Hints.typeclasses_db] ]
 END
 
 TACTIC EXTEND head_of_constr
@@ -93,16 +94,16 @@ TACTIC EXTEND fulleauto
     let dbs = match dbnames with [] -> ["typeclass_instances"]
                                | l -> l in
     let dbs = List.map Hints.searchtable_map dbs in
-    Class_tactics.new_eauto_tac false ?limit:depth dbs 
+    Class_tactics.new_eauto_tac false ?limit:depth true dbs
   ]
 | ["fulleauto" depth(depth) ] -> [
     let dbs = ["typeclass_instances"] in
     let dbs = List.map Hints.searchtable_map dbs in
-    Class_tactics.new_eauto_tac false ?limit:depth dbs 
+    Class_tactics.new_eauto_tac false ?limit:depth true dbs
   ]
 | ["fulleauto" ] -> [
     let dbs = ["typeclass_instances"] in
     let dbs = List.map Hints.searchtable_map dbs in
-    Class_tactics.new_eauto_tac false dbs 
+    Class_tactics.new_eauto_tac false true dbs
   ]
 END