Opened 10 years ago
Closed 9 years ago
#492 closed defect (fixed)
Proof General: script management confused, couldn't find goal span for save. when evaluating past the bottom of a module that contains a theorem with the same name as the module
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.3 |
Component: | 2:pg-emacs | Keywords: | coq coq-8.4 |
Cc: | jasongross9+pg@… |
Description
Here is a proof script that gives "Proof General: script management confused, couldn't find goal span for save." in PG 4.3pre131011 with Coq 8.4pl3 (December 2013):
Module match_beta. Theorem match_beta : True. Proof. exact I. Defined. End match_beta. Module foo.
Change History (3)
comment:1 Changed 9 years ago by
comment:2 Changed 9 years ago by
I can. It probably comes from the lemma and the Module having the same name.
comment:3 Changed 9 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Actually it came from the hacks for discriminating goal commands from others. the presence of "match" was checked (and counted compared to "with") and wrongly detected here despite the "_". Fixed.
Note: See
TracTickets for help on using
tickets.
Can you still reproduce this? I can't in the latest CVS. --cpitcla