Custom Query (361 matches)
Results (16 - 18 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #368 | needmoreinfo | coq, already defined values | ||
| Description |
Hi, The following code is rejected by Coq, since [x] is already defined in the second line, but proofgeneral "validates" it (it goes through, so that one has to be really careful to notice the warning in the "coq output" buffer - this can be quite errorprone since Coq keeps the old definition). << Definition x := 3. Definition x := 5. Damien |
|||
| #373 | needmoreinfo | PG 4.0 forgets things. | ||
| Description |
Something is going very, very wrong with the proof state... see screenshot. |
|||
| #431 | needmoreinfo | "This subproof is complete" appears at bottom of goals | ||
| Description |
After a bulleted subproof has been completed, This subproof is complete, but there are still unfocused goals: appears at the bottom of the goals window. It should either appear at the top, or not at all. |
|||
Note: See TracQuery
for help on using queries.
