Custom Query (361 matches)
Results (1 - 3 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #512 | fixed | test.coq target doesn't exist | ||
| Description |
In the coq subdirectory of PG, there's a file coq-autotest.el. In that file: ;; coq-autotest.el: tests of Coq Proof General (in progress). ;; You can run these by issuing "make test.coq" in PG home dir. That target does not exist in the main directory's Makefile. That behavior holds in PG 4.2 as well as the 4.3 preview I downloaded, 4.3pre150930. |
|||
| #511 | invalid | new Coq command "From" supported by PG? | ||
| Description |
When trying to use the new Coq command "From" (https://coq.inria.fr/distrib/V8.5pl1/refman/Reference-Manual008.html#hevea_command116), I get: Error: Unknown command of the non proof-editing mode. |
|||
| #505 | fixed | Fix indentation of lazymatch in Coq | ||
| Description |
Patch here: http://pastebin.com/u68uY13X |
|||
Note: See TracQuery
for help on using queries.
