]> matita.cs.unibo.it Git - helm.git/commitdiff
Fixed dependency function, which was lacking the code for recursive calls.
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 15 Jul 2009 13:29:33 +0000 (13:29 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 15 Jul 2009 13:29:33 +0000 (13:29 +0000)
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 [];;