X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.mli;h=47846f999b155e6d24415fd77687afbde4022bb0;hb=0581f3c8dc2098b82cd31a0fbed224a95652bd88;hp=5d496d9365f58480ac92c15323624cae9d214284;hpb=40ce8d1c14808ea7608ee2988bd9aba77ddf8200;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 5d496d936..47846f999 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
@@ -26,8 +26,18 @@ module Index (B : Terms.Blob) :
       type data = ClauseSet.elt and 
       type dataset = ClauseSet.t
     
-    val index_unit_clause :
-          DT.t -> B.t Terms.unit_clause -> DT.t 
+    val index_unit_clause : 
+      DT.t -> B.t Terms.unit_clause -> DT.t 
+
+    val remove_unit_clause :
+      DT.t -> B.t Terms.unit_clause -> DT.t 
+
+    val fold : 
+      DT.t ->
+      (B.t Discrimination_tree.path -> ClauseSet.t -> 'a -> 'a) 
+      -> 'a -> 'a
+
+    val elems : DT.t -> ClauseSet.t
 
     type active_set = B.t Terms.unit_clause list * DT.t