Release 0.5.9.

[helm.git] / helm / software / components / ng_paramodulation / index.mli

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