X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.mli;h=47846f999b155e6d24415fd77687afbde4022bb0;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=2fc8ec1e847323edd88f10681c83fc3f112bd9bc;hpb=449295993c1fb0732fd5b14a570f8c5260653164;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 2fc8ec1e8..47846f999 100644
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -32,6 +32,13 @@ module Index (B : Orderings.Blob) :
     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
 
   end