Opened 12 years ago
Last modified 12 years ago
#443 closed defect
Retracting, editing, then re-evaluating/proving sometimes results in definitions that do not match the contents of the file — at Initial Version
| Reported by: | coquser | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.2 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | jasongross9+bugzilla@… |
Description
I'm not sure whether this is a bug in Coq, or in Proof General.
Given the following file*:
Require Import Program Omega Bool.
Lemma bar : 128 * 128 + 128 = 16512.
compute; trivial.
Qed.
Lemma baz : 128 * 128 + 128 = 16512.
compute; trivial.
Qed.
Lemma qux : 128 * 128 + 128 = 16512.
compute; trivial.
Qed.
Lemma foo : forall x : Type, x = x.
auto.
Qed. Print foo. Print foo.
Tell Coq to evaluate the entire thing, then, after it evaluates the [Require Import], tell it to not evaluate [foo] (ctrl + c, ctrl + enter on the [Lemma foo] line), then quickly change [Type] to [nat] before it finishes the proof of [qux], and then tell it to evaluate down to [Print foo], again. When I [Print foo], it shows the original definition (with [Type]), rather than the new definition (with [nat]).
*This will only work on a sufficiently slow computer with a sufficiently fast person. You may need to add more filler theorems, or increase the size of the numbers, so that it slows down enough to change the word before it gets there. I'm doing this in emacs (GNU Emacs 23.1.50.1 (i386-mingw-nt6.1.7601) of 2009-11-03 on LENNART-69DE564 (patched)) running Proof General (Version 4.1), and I have an HP running Windows 7 x64 with 4 GB of RAM and an AMD Turion(tm) X2 Ultra Dual-Core Mobile ZM-87 2.40 GHz.
