]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/stats.ml
Fixed dependency function, which was lacking the code for recursive calls.
[helm.git] / helm / software / components / ng_paramodulation / stats.ml
index a281ddc867a12ee8a21ab8f1ae17f629cf345e87..0f9f45d960e6c30aac980d5bde0f62950d7678a1 100644 (file)
@@ -85,7 +85,7 @@ module Stats (B : Terms.Blob) =
 
     let rec dependencies op clauses acc =
       match clauses with
-       | [] -> []
+       | [] -> acc
        | (_,lit,_,_)::tl ->
            match lit with
              | Terms.Predicate _ -> assert false
@@ -109,7 +109,7 @@ module Stats (B : Terms.Blob) =
                            else
                              dependencies op tl acc
                        else dependencies op tl acc
-                   | _ -> acc
+                   | _ -> dependencies op tl acc
     ;;
 
     let dependencies op clauses = dependencies op clauses [];;