X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=30d32d540a330d8bdb9495b086a134e0fffd5391;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=c67dbfb07dbbc13b3297d0b8903305a9680cf588;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index c67dbfb07..30d32d540 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -15,11 +15,7 @@ module Superposition (B : Orderings.Blob) :
   sig
 
                         (* bag, maxvar, meeting point *)
-    exception Success of 
-      B.t Terms.bag 
-      * int 
-      * B.t Terms.unit_clause
-      * B.t Terms.substitution
+    exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
     (* The returned active set is the input one + the selected clause *)
     val infer_right :
@@ -64,6 +60,8 @@ module Superposition (B : Orderings.Blob) :
       B.t Terms.bag ->
       int ->
       B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
+
+
     val keep_simplified:
       B.t Terms.unit_clause ->
       Index.Index(B).active_set ->
@@ -77,8 +75,5 @@ module Superposition (B : Orderings.Blob) :
       B.t Terms.unit_clause ->
       bool
 
-    val are_alpha_eq : 
-      B.t Terms.unit_clause ->
-      B.t Terms.unit_clause ->
-      bool
+
   end