right inference step completed

[helm.git] / helm / software / components / ng_paramodulation / superposition.mli

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index 54b5ae50f322a031bc926de684e25539c9ec7204..adfaf68e299d539776cac2a6cddc8d966036af49 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -16,13 +16,13 @@ module Superposition (B : Terms.Blob) :
   sig
 
     (* The returned active set is the input one + the selected clause *)
-    val superposition_right :
+    val infer_right :
           B.t Terms.bag -> 
           int -> (* maxvar *)
           B.t Terms.unit_clause -> (* selected *)
           Index.Index(B).active_set ->
             B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
-                  
+
   end