New functorialization: paramod is abstracted over a Orderings.Blob, that is like...

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

diff --git a/helm/software/components/ng_paramodulation/foUnif.mli b/helm/software/components/ng_paramodulation/foUnif.mli
index 6d50f70ee2339087099df6da70d9540a044b59a4..87b57ae70d74b979e83e021cfbae75a95941951e 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.mli
+++ b/helm/software/components/ng_paramodulation/foUnif.mli
@@ -13,7 +13,7 @@
 
 exception UnificationFailure of string Lazy.t;;
 
-module Founif (B : Terms.Blob) : 
+module Founif (B : Orderings.Blob) : 
   sig
 
    val unification:
@@ -23,7 +23,7 @@ module Founif (B : Terms.Blob) :
      Terms.varlist -> 
      B.t Terms.foterm ->
      B.t Terms.foterm ->
-        B.t Terms.substitution * Terms.varlist
+        B.t Terms.substitution 
 
 
    val alpha_eq: