summaryrefslogtreecommitdiff
path: root/test-suite/ide
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/ide')
-rw-r--r--test-suite/ide/undo.v23
1 files changed, 23 insertions, 0 deletions
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 *)
+