X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.mli;h=36b5bd153a083ad99e86032c9ead1e1ddbefbe61;hb=88efee4c688d660d2205c5933d302770acb5b407;hp=99d6aa7e8cc44d1aed184cedbcca557c8c81c7f3;hpb=f00757144b2cd7e6457fed55dbc1309d11a542dc;p=helm.git diff --git a/helm/software/components/ng_tactics/nAuto.mli b/helm/software/components/ng_tactics/nAuto.mli index 99d6aa7e8..36b5bd153 100644 --- a/helm/software/components/ng_tactics/nAuto.mli +++ b/helm/software/components/ng_tactics/nAuto.mli @@ -15,4 +15,11 @@ val auto_tac: params:(NTacStatus.tactic_term list * (string * string) list) -> 's NTacStatus.tactic +val group_by_tac: + eq_predicate: + ((#NTacStatus.tac_status as 'a) -> + Continuationals.goal list -> Continuationals.goal -> bool) -> + action:'a NTacStatus.tactic -> + 'a NTacStatus.tactic + val debug : bool ref