X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.mli;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.mli;h=93517597fd518607326b0ed72e94c200c305cef9;hb=39a2078b0e835d39895a5b6c0862d668ece544f3;hp=51934d1b1f592a1afe69620a47a551ba8dbd0785;hpb=95a14ced97592a4116485f94c6ffa806feb62dbc;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 51934d1b1..93517597f 100644
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -14,7 +14,11 @@
 module Index (B : Orderings.Blob) : 
   sig
     module ClauseSet : Set.S with 
-      type elt = Terms.direction * B.t Terms.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
@@ -27,7 +31,7 @@ module Index (B : Orderings.Blob) :
       type dataset = ClauseSet.t
     
     val index_clause :
-          DT.t -> B.t Terms.clause -> DT.t 
+          DT.t -> B.t Terms.clause -> DT.t
 
     type active_set = B.t Terms.clause list * DT.t