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

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

diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index 05fdbe37cdca5b4b301a0e840890cc5337cf173a..427db4f95bfca6c911bb5b1f6d9cf5dd786430ef 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -25,8 +25,8 @@ let mem2 a b l =
    aux false false l
 ;;
 
-module Founif (B : Terms.Blob) = struct
-  module Subst = FoSubst (*.Subst(B)*)
+module Founif (B : Orderings.Blob) = struct
+  module Subst = FoSubst 
   module U = FoUtils.Utils(B)
 
   let unification vars locked_vars t1 t2 =