]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/superposition.mli
Various fixes
[helm.git] / helm / software / components / ng_paramodulation / superposition.mli
index bcfb0091e619e4784657aa8f05eb5b3252b67d3c..e3e2f8b9f2f6f15d12c791a4351309f022139ccd 100644 (file)
@@ -42,7 +42,7 @@ module Superposition (B : Terms.Blob) :
           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 :