From aca0bb7546310d87146d27f16b1e98699a23e085 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 12 Nov 2003 19:26:26 +0000
Subject: Restructuration ZArith

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4879 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/OmegaLemmas.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/omega/OmegaLemmas.v b/contrib/omega/OmegaLemmas.v
index 98922f3fd2..c292240699 100644
--- a/contrib/omega/OmegaLemmas.v
+++ b/contrib/omega/OmegaLemmas.v
@@ -78,7 +78,7 @@ Lemma OMEGA8:
 
 Intros x y H1 H2 H3; Elim (Zle_lt_or_eq ZERO x H1); [
   Intros H4; Absurd (Zlt ZERO x); [
-    Change (Zge ZERO x); Apply Zle_ge; Apply (Zsimpl_le_plus_l y);
+    Change (Zge ZERO x); Apply Zle_ge; Apply Zsimpl_le_plus_l with y;
     Rewrite -> H3; Rewrite Zplus_inverse_r; Rewrite Zero_right; Assumption
   | Assumption]
 | Intros H4; Rewrite -> H4; Trivial with arith].
-- 
cgit v1.2.3