From 7cb299f5c1b534246e92e99b39aa4e2b84fbb9e4 Mon Sep 17 00:00:00 2001 From: vgross Date: Fri, 26 Feb 2010 19:31:31 +0000 Subject: 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 --- test-suite/ide/undo.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'test-suite/ide') 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 *) + -- cgit v1.2.3