X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.mli;h=bfed8d533e73dfc9d315c7188d6ae6595154697a;hb=04ae8084273d40d58a391a5a530511c975fbd22d;hp=5581f7cfa7fd7bbcda4f39d56b00f56b4210c503;hpb=637114791874df9ebc4e0f0936513c71886a913f;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 5581f7cfa..bfed8d533 100644
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -11,7 +11,7 @@
 
 (* $Id$ *)
 
-module Index (B : Terms.Blob) : 
+module Index (B : Orderings.Blob) : 
   sig
     module ClauseSet : Set.S with 
       type elt = Terms.direction * B.t Terms.unit_clause
@@ -27,6 +27,8 @@ module Index (B : Terms.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
 
   end