labels in group_by_tac

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index c9162d0fe2080923a5f31deca1fd5ffb5ff7c626..e68f02d2ab71ed23f84e13fff033f180000feed2 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1375,7 +1375,7 @@ let auto_tac ~params:(_univ,flags) status =
     up_to 2 depth
 ;;
 
-let group_by_tac eq_predicate tactic status = 
+let group_by_tac ~eq_predicate ~action:tactic status = 
  let goals = head_goals status#stack in
  if List.length goals < 2 then tactic status 
  else
@@ -1425,7 +1425,7 @@ let type_dependency status gl g =
 ;;
 
 let auto_tac ~params = 
-  group_by_tac type_dependency (auto_tac ~params)
+  group_by_tac ~eq_predicate:type_dependency ~action:(auto_tac ~params)
 ;;
 
 (* ========================= dispatching of auto/auto_paramod ============ *)