]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/superposition.mli
snaphost: supright almost done
[helm.git] / helm / software / components / ng_paramodulation / superposition.mli
index c2c0ef43d0603be7c520331ffbd76fa80aae0f93..b67233563591d624f42bdaba3e1a2564f6b61e54 100644 (file)
 module Superposition (B : Terms.Blob) : 
   sig
 
-    val superposition_right_step :
+    val superposition_right_with_table :
           B.t Terms.bag -> 
+          int -> (* maxvar *)
           B.t Terms.unit_clause ->
           Index.Index(B).DT.t ->
-            B.t Terms.bag * B.t Terms.unit_clause list
+            B.t Terms.bag * int * B.t Terms.unit_clause list
                   
   end