From be2a030746e20744f9a317a31c7053bcfbb6e505 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 8 Jun 2009 18:56:48 +0000 Subject: [PATCH] ... --- helm/software/components/ng_paramodulation/superposition.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 6d10c86d8..b002dce33 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -16,6 +16,7 @@ module Superposition (B : Terms.Blob) = module IDX = Index.Index(B) module Unif = FoUnif.Founif(B) module Subst = FoSubst.Subst(B) + module Order = Orderings.Orderings(B) let all_positions t f = let rec aux pos ctx = function @@ -67,7 +68,9 @@ module Superposition (B : Terms.Blob) = let r = Subst.apply_subst subst r in let l = Subst.apply_subst subst l in let ty = Subst.apply_subst subst ty in - (0, Terms.Equation (l,r,ty,Terms.Incomparable), vl, proof)) + let o = Order.compare_terms l r in + (* can unif compute the right vl for both sides? *) + (0, Terms.Equation (l,r,ty,o), vl, proof)) res in (* fresh ID and metas and compute orientataion of new_clauses *) -- 2.39.2