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

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index bfed8d533..2fc8ec1e8 100644
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -26,8 +26,11 @@ module Index (B : Orderings.Blob) :
       type data = ClauseSet.elt and 
       type dataset = ClauseSet.t
     
-    val index_unit_clause :
-          int -> 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 
 
     type active_set = B.t Terms.unit_clause list * DT.t