X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=e3e2f8b9f2f6f15d12c791a4351309f022139ccd;hb=138af8ad1b6a6382606e367cc906f4232fa626ff;hp=6deb0a4eb7a07c7e090e856c35ffa76a8ceab732;hpb=a15dc157f7e63db12b9a7b59cf00aea108d7e073;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index 6deb0a4eb..e3e2f8b9f 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -39,22 +39,25 @@ module Superposition (B : Terms.Blob) :
 
     val simplify : 
           Index.Index(B).DT.t ->
+          int ->
           B.t Terms.bag ->
           B.t Terms.unit_clause ->
-            (B.t Terms.bag * B.t Terms.unit_clause) option
+            B.t Terms.bag * (B.t Terms.unit_clause option)
 
     (* may raise success *)
     val simplify_goal : 
           int ->
           Index.Index(B).DT.t ->
           B.t Terms.bag ->
+          B.t Terms.unit_clause list ->
           B.t Terms.unit_clause ->
-            B.t Terms.bag * B.t Terms.unit_clause
+            (B.t Terms.bag * B.t Terms.unit_clause) option
 
     val one_pass_simplification:
       B.t Terms.unit_clause ->
       Index.Index(B).active_set ->
       B.t Terms.bag ->
+      int ->
       (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
 
 
@@ -62,6 +65,7 @@ module Superposition (B : Terms.Blob) :
       B.t Terms.unit_clause ->
       Index.Index(B).active_set ->
       B.t Terms.bag ->
+      int ->
       (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option