X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fstats.mli;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fstats.mli;h=95fbe1d0c6a74c94ebd2591c22a8260afcd0b61b;hb=bebc917ebff72c2e235cb3062a4c94f10a9aab27;hp=271fd2bcf5c1011c0e0e62f5f50964ab9aa5ca26;hpb=b519aa529779c0a4625eb43fa9557862d8cc6617;p=helm.git diff --git a/helm/software/components/ng_paramodulation/stats.mli b/helm/software/components/ng_paramodulation/stats.mli index 271fd2bcf..95fbe1d0c 100644 --- a/helm/software/components/ng_paramodulation/stats.mli +++ b/helm/software/components/ng_paramodulation/stats.mli @@ -16,11 +16,11 @@ module Stats (B : Orderings.Blob) : module SymbMap : Map.S with type key = B.t - val parse_symbols : B.t Terms.unit_clause list -> (* hypotheses *) - B.t Terms.unit_clause -> (* goal *) + val parse_symbols : B.t Terms.clause list -> (* hypotheses *) + B.t Terms.clause -> (* goal *) (B.t * int * int * int * int list) list - val dependencies : B.t -> B.t Terms.unit_clause list -> B.t list + val dependencies : B.t -> B.t Terms.clause list -> B.t list end