X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.mli;h=36b5bd153a083ad99e86032c9ead1e1ddbefbe61;hb=3ca99dabf7d136ebd58fa61e7a2d7134c8dc365c;hp=f8f5ae4e212a40c234f0534fe9923bd8367615f0;hpb=39fb4421e9bea7f21f46c2fa1145c248c08d16b6;p=helm.git diff --git a/helm/software/components/ng_tactics/nAuto.mli b/helm/software/components/ng_tactics/nAuto.mli index f8f5ae4e2..36b5bd153 100644 --- a/helm/software/components/ng_tactics/nAuto.mli +++ b/helm/software/components/ng_tactics/nAuto.mli @@ -15,6 +15,11 @@ val auto_tac: params:(NTacStatus.tactic_term list * (string * string) list) -> 's NTacStatus.tactic -val auto_paramod_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