]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/index.mli
snaphost: supright almost done
[helm.git] / helm / software / components / ng_paramodulation / index.mli
index 3f86cc1e02bb5f3a569b6067b396649b5792017d..5581f7cfa7fd7bbcda4f39d56b00f56b4210c503 100644 (file)
@@ -25,5 +25,8 @@ 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 
 
   end