diff options
| author |  vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-26 19:31:31 +0000 |
|---|---|---|
| committer | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-26 19:31:31 +0000 |
| commit | 7cb299f5c1b534246e92e99b39aa4e2b84fbb9e4 (patch) | |
| tree | e00a6b0f216d952c32d103d116e38653f3275426 /test-suite/ide | |
| parent | af0f9fd3a43824d4e86b36a784619736478f4c83 (diff) | |
New backtracking code + fix bug #2082.
Previous code checkings were too lax, and information was lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/ide')
| -rw-r--r-- | test-suite/ide/undo.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v index 60c2e6579..d5e9ee5e8 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 *) + |