| Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
Like CHANGES, and the test-suite folder, this file receives too many
updates to have a code owner. It is the job of the reviewer of the PR
to review changes to these files as well.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
AppVeyor fail.
|
|
|
|
|
|
|
|
|
|
For instance, error in "Goal forall a f, f a = 0" is now located.
|
|
- The case 0 makes the code of intros until (and in particular of
Detyping.lookup_quantified_hypothesis_as_displayed more complicated).
- The introduction pattern "*" is compositional while "until 0" is not.
|
|
|
|
|
|
|
|
The script now performs many more checks and reports errors in
a more intelligible way.
|
|
|
|
In particular, don't use the GitHub interface. Also, not all reviews are
mandatory in some corner cases.
|
|
too long.
|
|
|
|
to coq, coqchk, coqdoc
|
|
|
|
|
|
|
|
|
|
Sphinx doc chapter 22
|
|
|
|
Sphinx doc chapter 21
|
|
|
|
Sphinx doc chapter 19
|
|
|
|
Sphinx doc chapter 17
|
|
Guillaume and I agreed to switch, as the new Sphinx infrastructure
changes this component significantly.
|
|
Thanks to Paul Steckler for porting this chapter.
|
|
|
|
Thanks to Pierre Letouzey for porting this chapter.
|
|
|
|
Thanks to Laurent Théry for porting this chapter.
|
|
|
|
Thanks to Clément Pit-Claudel for porting this chapter.
|
|
|
|
|
|
|
|
|
|
|