First tests for paramodulation (pretty printer, unification)

[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 048d082c558ab1f5b540b90ac4552867ab8c2b9f..bcea59ad57c02acde74bbef56614c3a0d623a041 100644 (file)
--- a/helm/software/components/ng_paramodulation/founif.ml
+++ b/helm/software/components/ng_paramodulation/founif.ml
@@ -14,7 +14,7 @@
 exception UnificationFailure of string Lazy.t;;
 
 module Founif (B : Terms.Blob) = struct
-  module Subst = Subst.Subst(B)
+  module Subst = Fosubst.Subst(B)
   module U = Terms.Utils(B)
 
   let unification vars locked_vars t1 t2 =