Custom Query (361 matches)
Results (4 - 6 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #154 | fixed | "restart" doesn't work | ||
| Description |
if i have an active scripting document, and then i restart, i cannot send any commands. i get the following errors: Exception when looking for a command. null Document not parsed far enough, invalid target position given or missing parse data: 0 probably some fields aren't being cleared. |
|||
| #460 | worksforme | proof general hanging on Coq Definition in file generated by Why3 | ||
| Description |
When I try to process the attached Coq file using ProofGeneral, it gets hung up on the Definition of IB6_IB7_QueryTags_First. In contrast, coqtop file works on this file. The file was generated by Why3's Coq driver, so maybe it's doing something that's syntactically unusual. I'm running PG 4.1 on GNU Emacs 24.2.1. The Coq version is 8.3pl4. |
|||
| #467 | fixed | The "Time (tactic)." vernacular command no longer displays timings unless the tactic finishes the proof | ||
| Description |
It used to be the case (and still is the case in coqtop) that Goal True /\ True. split. Time idtac. Time constructor. Time constructor.
would display the timings of all three |
|||
