X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=6deb0a4eb7a07c7e090e856c35ffa76a8ceab732;hb=7477c3dbbc2fafe248d48302be0d6ba4cb38d062;hp=23477be1a00d3d03b016d42520b69b6d8c7fa145;hpb=3a4481e963c6b6e78ad1dce05d75bea992ceaaed;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index 23477be1a..6deb0a4eb 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -51,7 +51,18 @@ module Superposition (B : Terms.Blob) :
           B.t Terms.unit_clause ->
             B.t Terms.bag * B.t Terms.unit_clause
 
-  end
+    val one_pass_simplification:
+      B.t Terms.unit_clause ->
+      Index.Index(B).active_set ->
+      B.t Terms.bag ->
+      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+
 
+    val keep_simplified:
+      B.t Terms.unit_clause ->
+      Index.Index(B).active_set ->
+      B.t Terms.bag ->
+      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
 
 
+  end