diff options
| -rw-r--r-- | test-suite/success/Omega.v | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index 0132a9c894..19bb5f809c 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. |