From b690cf1a76d33afc878ba9a51de414560209e8e8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 18 Jan 2002 16:50:32 +0000
Subject: Bug MERGE_EQ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2416 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/omega.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index 6d78494a22..23236bc3cc 100755
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -225,6 +225,9 @@ let map_eq_afine f e =
 
 let negate_eq = map_eq_afine (fun x -> -x)
 
+let opposite x y =
+  map_eq_linear (fun x -> - x) x.body = y.body & x.constant = y.constant
+
 let rec sum p0 p1 = match (p0,p1) with 
   | ([], l) -> l | (l, []) -> l
   | (((x1::l1) as l1'), ((x2::l2) as l2')) -> 
@@ -406,7 +409,7 @@ let redundancy_elimination system =
   let accu_ineq = ref [] in
   iter
     (fun p0 p1 -> match (p0,p1) with 
-       | (e, (Some x, Some y)) when x.constant = -y.constant -> 
+       | (e, (Some x, Some y)) when opposite x y ->
            let id=new_id () in
            add_event (MERGE_EQ(id,x,y.id));
            push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq
-- 
cgit v1.2.3