diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-21 09:32:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-21 09:32:43 +0000 |
| commit | a275d218ee58185d55bbd702b36e4d63cb33670d (patch) | |
| tree | f2cf4ecdc4527fb2712553ccc396dc75c40ff3d6 /contrib | |
| parent | 6f0399df592d58987a65e9e8fce857d80a2c4c22 (diff) | |
Correction de Pierre Crégut pour le bug MERGE_EQ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2421 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/omega/omega.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml index 23236bc3c..33ca60cb2 100755 --- a/contrib/omega/omega.ml +++ b/contrib/omega/omega.ml @@ -225,9 +225,6 @@ 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')) -> @@ -409,7 +406,7 @@ let redundancy_elimination system = let accu_ineq = ref [] in iter (fun p0 p1 -> match (p0,p1) with - | (e, (Some x, Some y)) when opposite x y -> + | (e, (Some x, Some y)) when x.constant = y.constant -> 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 |