Ajout exemple JCF conflit variable interne, variable de section

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2764 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 3 deletions

diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 0132a9c89..19bb5f809 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -26,8 +26,21 @@ Intros.
 Omega.
 Qed.
 
-(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *)
+(* Proposed by Jean-Christophe Filliātre: confusion between an Omega *)
+(* internal variable and a section variable (June 2001) *)
+
 Section A.
+Variable x,y : Z.
+Hypothesis H : `x > y`.
+Lemma lem4 : `x > y`.
+Omega.
+Qed.
+End A.
+
+(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *)
+(* May 2002 *)
+
+Section B.
 Variables R1,R2,S1,S2,H,S:Z.
 Hypothesis I:`R1 < 0`->`R2 = R1+(2*S1-1)`.
 Hypothesis J:`R1 < 0`->`S2 = S1-1`.
@@ -35,7 +48,7 @@ Hypothesis K:`R1 >= 0`->`R2 = R1`.
 Hypothesis L:`R1 >= 0`->`S2 = S1`.
 Hypothesis M:`H <= 2*S`.
 Hypothesis N:`S < H`.
-Lemma lem4 : `H > 0`.
+Lemma lem5 : `H > 0`.
 Omega.
 Qed.
-End A.
+End B.