| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We put it in a footnote otherwise the sentence was starting to be really long.
Footnotes need to be in index.rst to really appear at the bottom of the index page.
|
|
|
|
|
|
|
|
It was broken and undocumented. We dropped the git logs, too, so it wasn't clear
who wrote it and why it was introduced in the first place.
|
|
|
|
|
|
|
|
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
|
We split a Require Import in two to avoid reaching the timeout.
|
|
|
|
|
|
Move credits to its own chapter (closes #6573).
|
|
|
|
|
|
|
|
|
|
|
|
Fix #5012.
|
|
Closes GH-7742.
|
|
|
|
|
|
Many still remain.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Cf. Enrico's remark at https://github.com/coq/coq/pull/7536#issuecomment-389826121
This commit also marginally improves the Record doc (a lot more remains to do).
|
|
|
|
|
|
|
|
Including adding missing irrefutable-patterns to the grammar of binders.
|
|
As discussed in GH-7556.
|
|
|
|
It failed to compile before because the type arguments were declared implicit after introducing the notation
|
