| Age | Commit message (Expand) | Author |
| 2020-04-20 | Remove coqremote stylesheets which were useless since the Sphinx migration. | Théo Zimmermann |
| 2019-06-17 | Update copyright years outside of headers. | Théo Zimmermann |
| 2019-05-21 | Fixing typos - Part 1 | JPR |
| 2019-03-14 | Documentation for SProp | Gaëtan Gilbert |
| 2019-02-21 | Stdlib HTML documentation: fix a few absolute URLs | Vincent Laporte |
| 2019-01-29 | Use \mathcal instead of \cal | Gaëtan Gilbert |
| 2018-02-20 | Extended documentation for notations referring to binders. | Hugo Herbelin |
| 2017-11-25 | Updating the current official writing of OCaml, updating Camlp4->Camlp5. | Hugo Herbelin |
| 2017-10-25 | Put newlines at the end of files. | Gaëtan Gilbert |
| 2017-10-06 | Fix copyright info in reference manual. | Théo Zimmermann |
| 2017-08-23 | Update coypright dates on documentation | Matthieu Sozeau |
| 2017-08-02 | Port ssr manual to Coq's latex/hevea style | Enrico Tassi |
| 2017-08-02 | Makefile.doc: implement serve-refman-8080 target | Enrico Tassi |
| 2017-03-23 | Documenting the grammar {| ... |} syntax for building records. | Hugo Herbelin |
| 2016-12-06 | Fix broken documentation in presence of \zeroone{... \tt ...}. | Guillaume Melquiond |
| 2016-11-30 | Update copyright on documentation cover. | Maxime Dénès |
| 2016-04-24 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-04-12 | FIX: HTML version of Chapter 4 of the Reference Manual | Matej Kosik |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-14 | Updating and improving the documentation of intros patterns. | Hugo Herbelin |
| 2015-12-10 | ENH: examples for 'strict positivity' were expanded | Matej Kosik |
| 2015-12-10 | CLEANUP: s/List_A/List~A/g | Matej Kosik |
| 2015-12-10 | CLEANUP: superfluous examples were removed | Matej Kosik |
| 2015-12-10 | ENH: new example: "even" | Matej Kosik |
| 2015-12-10 | ALPHA-CONVERSION: s/Length/has_length/g | Matej Kosik |
| 2015-12-10 | ENH: The beginning of Section 4.5 (Inductive declarations) was changed in ord... | Matej Kosik |
| 2015-12-10 | RefMan, ch. 4: Removing the local context of inductive definitions. | Hugo Herbelin |
| 2015-12-10 | RefMan, ch. 4: Adding discharging of inductive types. | Hugo Herbelin |
| 2015-12-10 | RefMan, ch. 4: In chapter 4 about CIC, renounced to keep a local | Hugo Herbelin |
| 2015-12-10 | RefMan, ch. 4: Reformulating introduction of the chapter on CIC, being | Hugo Herbelin |
| 2015-07-31 | Remove some outdated files and fix permissions. | Guillaume Melquiond |
| 2015-02-17 | Separate index for vernacular options. | Maxime Dénès |
| 2015-01-13 | Refresh some copyright headers. | Maxime Dénès |
| 2015-01-05 | Added more informative messages about bullets. | Pierre Courtieu |
| 2014-12-09 | refman: switch all source files to utf8 | Pierre Letouzey |
| 2014-12-09 | refman: remove ?uri=referer in urls pointing to validator.w3.org | Pierre Letouzey |
| 2014-12-09 | refman: xhtml validity of the cover page | Pierre Letouzey |
| 2014-12-09 | doc: improved xhtml compatibility (cover, header,...) | Pierre Letouzey |
| 2014-12-09 | doc/stdlib: fix the html charset in header.html and co | Pierre Letouzey |
| 2014-12-09 | doc: version number in cover.html + updates in coq.inria.fr style | Pierre Letouzey |
| 2014-12-09 | Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la document... | notin |
| 2014-12-09 | Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat... | notin |
| 2014-11-07 | doc: version number in cover.html + updates in coq.inria.fr style | Pierre Letouzey |
| 2014-08-05 | Making references to Proof General and CoqIDE uniform in Reference Manual. | Hugo Herbelin |
| 2012-09-16 | Beautify tactic documentation a bit more. | gmelquio |
| 2012-09-16 | Remove superfluous spaces and commas in tactic documentation. | gmelquio |
| 2012-08-11 | Improving rendering of ldots in doc (partially done, there are too | herbelin |
| 2012-08-11 | Added support for option Local (at module level) in Tactic Notation. | herbelin |
| 2012-08-11 | Improving rendering of ...-separated lists and sequences in reference | herbelin |