From 6b17247776e8cf3b4b8660631c41279a6c5a7296 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 12 Jun 2002 17:57:06 +0000 Subject: Note of another bug --- etc/coq/nested.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'etc/coq') diff --git a/etc/coq/nested.v b/etc/coq/nested.v index 975101cd..f0d625b3 100644 --- a/etc/coq/nested.v +++ b/etc/coq/nested.v @@ -1,5 +1,11 @@ (* Nested Proofs, and backtrack mechanism in general. Bugs: + + - Undo of "Require Omega" in proof uses Undo instead of Back. + [ coq-count-undos needs fixing to use Back as well as Undo ? ] + +======= Below here fixed? + - once point 12 is reached, sould have one block from 3 to 12. With the goalsave test : OK but the reset command is wrong. @@ -19,11 +25,14 @@ Require List. (* 2 This needs "Back 1" to be retracted *) Lemma t1: (n: nat ) {n=O} + {(EX y | n = (S y))}. (* 3 This needs "Restart" to be retracted if inside the proof, and -"Reset t1. Back 3." if outside (after point 12). 3 because of the +"Reset t1. Back 4." if outside (after point 12). 3 because of the Require and the two lemmas inside the proof. If only "Reset t1", like with the current version of PG, then t2 and t3 are still in the environment. Try this with the current version and with my patch *) +(* da: Back command seems much better behaved than "Reset", which + always clears proof state, I think. Should PG always use Back? *) + Intros. (* 4 This needs "Undo" to be retracted *) Case n. (* 5 "Undo" *) EAuto. (* 6 "Undo" *) -- cgit v1.2.3