| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
Chapter ported by Théo Zimmermann and Maxime Dénès.
|
| |
|
|
|
|
|
|
| |
Thanks to Clément Pit Claudel for porting this chapter.
Backport universe polymorphism changes from 2017 and 2018.
|
|
|
|
| |
Thanks to Yves Bertot for porting this chapter.
|
|
|
|
| |
Thanks to Laurent Théry for porting this chapter.
|
|
|
|
| |
Thanks to Laurent Théry for porting this chapter.
|
|
|
|
| |
Thanks to Paul Steckler for porting this chapter.
|
|
|
|
| |
Thanks to Paul Steckler for porting this chapter.
|
|
|
|
| |
Thanks to Calvin Beck for porting this chapter.
|
|
|
|
| |
Thanks to Laurent Théry for porting this chapter.
|
|
|
|
| |
Thanks to Paul Steckler for porting this chapter.
|
|
|
|
| |
Thanks to Matthieu Sozeau for porting this chapter.
|
|
|
|
| |
Thanks to Pierre Letouzey for porting this chapter.
|
|
|
|
| |
Thanks to Pierre Letouzey for porting this chapter.
|
| |
|
|\ |
|
| |\ |
|
| | |\ |
|
| | | |
| | | |
| | | |
| | | | |
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.
|
|
|
|
|
| |
Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot
for porting this chapter.
|
|
|
|
| |
Thanks to Pierre Letouzey for porting this chapter.
|
|
|
|
| |
Thanks to Paul Steckler for porting this chapter.
|
|
|
|
| |
Thanks to Paul Steckler for porting this chapter.
|
|
|
|
| |
Thanks to Paul Steckler for porting this chapter.
|
|
|
|
| |
Thanks to Clément Pit-Claudel for porting this chapter.
|
|
|
|
| |
Thanks to Calvin Beck for porting this chapter.
|
|
|
|
| |
Thanks to Heiko Becker and Nikita Zyuzin for porting this chapter.
|
|
|
|
| |
Thanks to Richard Ford for porting this chapter.
|
|
|
|
| |
Thanks to Richard Ford for porting this chapter.
|
|
|
|
| |
Thanks to Paul Steckler for porting this chapter.
|
| |
|
|
|
|
| |
I backported changes done to the LaTeX manual.
|
| |
|
| |
|
| |
|
| |
|
|
The original contribution is from Clément Pit-Claudel. I updated
his code and integrated it with the Coq build system. Many improvements
by Paul Steckler (MIT).
This commit adds the infrastructure but no content.
|