The new paramodulation functions instantiated over nCic.

[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 7d75f28370d00eb487764e4e8d87cd5b18c40f33..2fc8ec1e847323edd88f10681c83fc3f112bd9bc 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -26,8 +26,11 @@ module Index (B : Orderings.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_unit_clause : 
+      DT.t -> B.t Terms.unit_clause -> DT.t 
+
+    val remove_unit_clause :
+      DT.t -> B.t Terms.unit_clause -> DT.t 
 
     type active_set = B.t Terms.unit_clause list * DT.t