statistics are used, when possible, to sort

[helm.git] / helm / software / components / ng_paramodulation / stats.mli

diff --git a/helm/software/components/ng_paramodulation/stats.mli b/helm/software/components/ng_paramodulation/stats.mli
index b9be72907943a4c4ab6dfb1c2421b0133ac5878e..271fd2bcf5c1011c0e0e62f5f50964ab9aa5ca26 100644 (file)
--- 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