first proof reconstruction attempt, still bugged since it

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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 046799a775149470bd7162252b023e582ffb9e99..2198ec8bd2be1a3fda3ccf8bd17b770b65655d02 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -15,7 +15,7 @@ module Superposition (B : Terms.Blob) =
   struct
     module IDX = Index.Index(B)
     module Unif = FoUnif.Founif(B)
-    module Subst = FoSubst.Subst(B)
+    module Subst = FoSubst (*.Subst(B)*)
     module Order = Orderings.Orderings(B)
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)