From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- test-suite/ide/undo.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'test-suite/ide/undo.v') diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v index 60c2e657..d5e9ee5e 100644 --- a/test-suite/ide/undo.v +++ b/test-suite/ide/undo.v @@ -77,3 +77,26 @@ Qed. Definition q := O. Definition r := O. + +(* Bug 2082 : Follow the numbers *) + +Variable A : Prop. +Variable B : Prop. + +Axiom OR : A \/ B. + +Lemma MyLemma2 : True. +proof. +per cases of (A \/ B) by OR. +suppose A. + then (1 = 1). + then H1 : thesis. (* 4 *) + thus thesis by H1. (* 2 *) +suppose B. (* 1 *) (* 3 *) + then (1 = 1). + then H2 : thesis. + thus thesis by H2. +end cases. +end proof. +Qed. (* 5 if you made it here, there is no regression *) + -- cgit v1.2.3