X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.mli;h=9bd662b19656cea483d182411d4c4275d91791b8;hb=946065280df015323ce624769fd0c4261f8b4209;hp=30d32d540a330d8bdb9495b086a134e0fffd5391;hpb=449295993c1fb0732fd5b14a570f8c5260653164;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index 30d32d540..9bd662b19 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -60,8 +60,6 @@ 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 ->
@@ -75,5 +73,8 @@ 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