diff options
Diffstat (limited to 'etc/coq')
| -rw-r--r-- | etc/coq/nested.v | 11 |
1 files changed, 10 insertions, 1 deletions
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" *) |