One-side indexing for commutativity

[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 3f86cc1e02bb5f3a569b6067b396649b5792017d..bfed8d533e73dfc9d315c7188d6ae6595154697a 100644 (file)
--- 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
@@ -25,5 +25,10 @@ module Index (B : Terms.Blob) :
       type input = B.t Terms.foterm and 
       type data = ClauseSet.elt and 
       type dataset = 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
 
   end