| Age | Commit message (Collapse) | Author |
|---|
|
This makes `coqidetop` behavior consistent with the one of
`coqtop`.
This was likely needed in the past when Coq used to print all kind of
stuff to stdout, including goal display. Now, it is not the case
anymore and this flag mainly controls printing verbosity.
|
|
|
|
|
|
|
|
function
|
|
Simpler
|
|
Actually there are more general instructions
|
|
|
|
|
|
|
|
|
|
|
|
bypassing dependencies
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
symlink from repo
|
|
And marginal improvements in the last section of the Gallina chapter.
|
|
We never actually used the -warn-error flag...
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Following the migration to Gitlab (#6919) we reduce Circle load, see
also discussion in #7436 and #7482.
|
|
This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
|
|
|
|
Fixes #7065
|
|
only-printing declarations.
|
|
|
|
|
|
It's redundant as a dependency of formal-topology.
|
|
|
|
|
|
Not only are most of "forall"s in the manual in Coq notation, but the
math notation leads to have a specially long space after the comma.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
