Fixed conflicts due to problem when merging with UEQ implementation

[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 5d496d9365f58480ac92c15323624cae9d214284..93517597fd518607326b0ed72e94c200c305cef9 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -11,10 +11,14 @@
 
 (* $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
+      type elt =
+          Terms.direction * (* direction if it is an equality *)
+         bool *            (* true if indexed literal is positive *)
+         int *             (* position of literal in clause *)
+         B.t Terms.clause
 
     module FotermIndexable : Discrimination_tree.Indexable with 
       type constant_name = B.t and
@@ -26,9 +30,9 @@ 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_clause :
+          DT.t -> B.t Terms.clause -> DT.t
 
-    type active_set = B.t Terms.unit_clause list * DT.t
+    type active_set = B.t Terms.clause list * DT.t
 
   end