From a9cd28741dda5eaf168ed488c0ca118e91115a0b Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 25 Jan 2002 10:28:59 +0000
Subject: patch Omega (bug 129)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2436 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/coq_omega.ml | 2 +-
 contrib/omega/omega.ml     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 729b3278d9..08ed476988 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1161,7 +1161,7 @@ let replay_history tactic_normalisation =
 	  let kk = mk_integer k in
 	  let state_eq = mk_eq eq1 (mk_times eq2 kk) in
 	  if e1.kind = DISE then
-            let tac = scalar_norm [P_APP 1] e2.body in
+            let tac = scalar_norm [P_APP 3] e2.body in
             tclTHENS 
 	      (cut state_eq) 
 	      [tclTHEN 
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index 33ca60cb24..70ee08ddd6 100755
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -279,7 +279,7 @@ let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) =
       let d = x - c * gcd in
       let new_eq = {id=id; kind=eq_flag; constant=c; 
                     body=map_eq_linear (fun c -> c / gcd) e} in
-      add_event (if eq_flag=EQUA then EXACT_DIVIDE(eq,gcd)
+      add_event (if eq_flag=EQUA or eq_flag = DISE then EXACT_DIVIDE(eq,gcd)
                  else DIVIDE_AND_APPROX(eq,new_eq,gcd,d));
       [new_eq]
     end else [eq]
-- 
cgit v1.2.3