aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2004-12-29 12:09:14 +0000
committerherbelin2004-12-29 12:09:14 +0000
commit21a985b7bbd6160b5b7b12992e810191cb4dfd76 (patch)
tree5d65f355e5f5d1749a5849a1ff03bb8b7882b04a
parentd364540c950a659c7d28267d1a979cbd91f0ebc6 (diff)
Bug transformation assert dans commit précédent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6522 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xcontrib/omega/omega.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index 4eaab67b2a..84239e03c0 100755
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -618,7 +618,7 @@ let negation (eqs,ineqs) =
let {body=ne;constant=c} ,kind = normal e in
Hashtbl.add table (ne,c) (kind,e)) diseq;
List.iter (fun e ->
- assert (e.kind <> EQUA);
+ assert (e.kind = EQUA);
let {body=ne;constant=c},kind = normal e in
try
let (kind',e') = Hashtbl.find table (ne,c) in