| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
As suggested by @herbelin.
|
|
|
|
|
|
|
|
|
|
|
|
Also includes a minor fix of the Extraction doc (a Require was missing).
|
|
Minor clean up, no sense in having these as they do nothing.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We document the most useful timing targets and variables, how to invoke
them, and what the output looks like.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We document an example `Makefile` which does not include the generated
`CoqMakefile`, but instead invokes arbitrary targets in it.
|
|
It does not seem to be referred to by any file, and does not seem to be
built by any implicit rules.
|
|
|
|
As suggested by @psteckler.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971
|
|
|
|
|
|
|
