From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 8 Jun 2009 18:56:48 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3905
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=be2a030746e20744f9a317a31c7053bcfbb6e505;p=helm.git

...
---

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 *)