first proof reconstruction attempt, still bugged since it

[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 fae6e084037d44439145679ea9aa036815524971..6eb014062f81451292249ac8382e8272da65cc58 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 = FoSubst.Subst(B)
+  module Subst = FoSubst (*.Subst(B)*)
   module U = FoUtils.Utils(B)
 
   let unification vars locked_vars t1 t2 =