From 7f29d7713208180a1b09b3f903c1b5fd8ec4c896 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 Jun 2009 14:44:21 +0000 Subject: [PATCH] ... --- helm/software/components/ng_paramodulation/superposition.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 84de696df..d3e6000b7 100644 --- 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 module Order = Orderings.Orderings(B) module Utils = FoUtils.Utils(B) module Pp = Pp.Pp(B) @@ -133,7 +133,6 @@ module Superposition (B : Terms.Blob) = ;; let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table = - (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*) match literal with | Terms.Predicate t -> assert false | Terms.Equation (l,r,ty,_) -> -- 2.39.2