]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/stats.mli
First compiling version
[helm.git] / helm / software / components / ng_paramodulation / stats.mli
index 271fd2bcf5c1011c0e0e62f5f50964ab9aa5ca26..95fbe1d0c6a74c94ebd2591c22a8260afcd0b61b 100644 (file)
@@ -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