Custom Query (361 matches)
Results (61 - 63 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #285 | fixed | byte compilation | ||
| Description |
GNU Emacs 23.1.1 on Mac OS, Proof General 4.0pre090902 (or CVS version).
Byte compilation via (Since only GNU Emacs is supported now, I wonder if byte compilation could be made the default.) |
|||
| #406 | upstream | auto compile bugs when some outputs is done by coqc | ||
| Description |
To reproduce the bug: 1) have in file foo.v the following: Eval compute in 0. 2) Have in file bar.v the following: Require Import foo. 3) then try to script bar.v (with auto-compilation on), compilation of foo.v is started automatically but then there is an error due to the read-only status of coq-compile-response buffer. I think this is due to the fact that coqc compilation *does* the output. Cheers, P. excerpt of buffer *Messages*: Check /home/courtieu/titi.vo Recompile /home/courtieu/titi.v Waiting for process to die...done condition-case: Buffer is read-only: #<buffer *coq-compile-response*> |
|||
| #400 | fixed | assert newly added text in ancestor fails | ||
| Description |
See the test case in coq/ex/test-cases/change-ancestor/README. The problem appears when one asserts text that has just been added at the end of an completely locked ancestor. Then Proof General sends only the newly added portion to Coq instead of the complete buffer. |
|||
