X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fstats.mli;h=271fd2bcf5c1011c0e0e62f5f50964ab9aa5ca26;hb=4244a4d70b9ab2fece0ff5b63506f6d323cbfbe2;hp=b9be72907943a4c4ab6dfb1c2421b0133ac5878e;hpb=6f2f9693db45a2ef905123bc48cde9f04ddff54f;p=helm.git diff --git a/helm/software/components/ng_paramodulation/stats.mli b/helm/software/components/ng_paramodulation/stats.mli index b9be72907..271fd2bcf 100644 --- a/helm/software/components/ng_paramodulation/stats.mli +++ b/helm/software/components/ng_paramodulation/stats.mli @@ -18,7 +18,7 @@ module Stats (B : Orderings.Blob) : val parse_symbols : B.t Terms.unit_clause list -> (* hypotheses *) B.t Terms.unit_clause -> (* goal *) - (B.t * int * int * int) list + (B.t * int * int * int * int list) list val dependencies : B.t -> B.t Terms.unit_clause list -> B.t list