X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.mli;h=bfed8d533e73dfc9d315c7188d6ae6595154697a;hb=50ed5ab75a38693c7b7558ca9487998e81bb7f89;hp=7d75f28370d00eb487764e4e8d87cd5b18c40f33;hpb=2bcf927f58bac034b8758173cdbd16cb7475de36;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 7d75f2837..bfed8d533 100644
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -27,7 +27,7 @@ module Index (B : Orderings.Blob) :
       type dataset = ClauseSet.t
     
     val index_unit_clause :
-          DT.t -> B.t Terms.unit_clause -> DT.t 
+          int -> DT.t -> B.t Terms.unit_clause -> DT.t 
 
     type active_set = B.t Terms.unit_clause list * DT.t