X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.mli;h=5d496d9365f58480ac92c15323624cae9d214284;hb=a232a59672817abd3d6ec07db0b20d8b3fe5ad3b;hp=3f86cc1e02bb5f3a569b6067b396649b5792017d;hpb=6c4056ea40b96039f24eeda9a1e1900c95bad7c8;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 3f86cc1e0..5d496d936 100644
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -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 :
+          DT.t -> B.t Terms.unit_clause -> DT.t 
+
+    type active_set = B.t Terms.unit_clause list * DT.t
 
   end