Custom Query (361 matches)
Results (19 - 21 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #373 | needmoreinfo | PG 4.0 forgets things. | ||
| Description |
Something is going very, very wrong with the proof state... see screenshot. |
|||
| #374 | invalid | cannot turn on electric-terminator interactively | ||
| Description |
I seem to be able to enable the electric-terminator using a hook in my .emacs file (although it doesn't work right -- see issue 371), but "C-c ;" gives me "C-c ; is undefined". |
|||
| #375 | invalid | PG goes into infinite loop with 100% CPU usage | ||
| Description |
To reproduce: download the attachment. Then type: emacs -nw pg_bug3.v Pick your nose while admiring the cromulent proof general splash screen. Type "C-c ." to turn on electric terminator. Move to the end of the file. Delete the existing period and re-type it. Type a new period. Watch your computer furiously increase the entropy level in the room. FWIW, executing "coqc pg_bug3.v" reports an error, so this script clearly is not valid. However, the fact that PG goes into a 100% CPU usage situation is probably not the best reaction. |
|||
