From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 28 Oct 2009 12:22:10 +0000 (+0000)
Subject: labels in group_by_tac
X-Git-Tag: make_still_working~3249
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=84898a3fec4588250f41e406338cbef64e60f20d;p=helm.git

labels in group_by_tac
---

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index c9162d0fe..e68f02d2a 100644
--- 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 ============ *)