| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The FAQ is not part of the Coq sources anymore.
|
|
|
|
Following up on #6791, we the option "Discriminate Introduction".
|
|
Following up on #6791, we the option "Shrink Abstract".
|
|
a record.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Instead of using a command-analysis heuristic, coqtop will now print
goals if the goal has changed. We use a fast goal comparison
heuristic, but a more refined strategy would be possible.
This brings some [IMHO very welcome] change to PG and `-emacs`, which
will now disable the printing of goals. Now, instead of playing with
`Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show`
command whenever it wishes to redisplay the goals.
This change will break PG, so we need to carefully coordinate this PR
with PG upstream (see ProofGeneral/PG#212).
Some interesting further things to do:
- Detect changes in nested proofs.
- Uncouple the silent flag from "print goals".
|
|
gtksourceview depends transitively on py2cairo which was updated in
Homebrew to depend explicitly on python2 (see Homebrew/homebrew-core#24714):
this makes the python3 install step impossible.
We also remove the libxml2 install step which was failing in a non-fatal way.
|
|
|
|
|
|
|
|
ocamldoc chokes on the markers {{{ and }}} because { and } are part of
its syntax
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
