From 84898a3fec4588250f41e406338cbef64e60f20d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2009 12:22:10 +0000 Subject: [PATCH] labels in group_by_tac --- helm/software/components/ng_tactics/nAuto.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 ============ *) -- 2.39.2