| Age | Commit message (Expand) | Author |
| 2017-06-15 | Merge PR#375: Deprecation | Maxime Dénès |
| 2017-06-14 | Merge PR#765: Remove obsolete Show commands | Maxime Dénès |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey |
| 2017-06-14 | Remove support for Coq 8.4. | Guillaume Melquiond |
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey |
| 2017-06-12 | Remove commented documentation for Show Tree. | Théo Zimmermann |
| 2017-06-01 | Merge PR#449: make specialize smarter (bug 5370). | Maxime Dénès |
| 2017-05-31 | Documenting the new behaviour of specialize. | Pierre Courtieu |
| 2017-05-30 | Documentation for eassert, eenough, epose proof, eset, eremember, epose. | Hugo Herbelin |
| 2017-05-27 | Documenting the existence of first and solve as Ltac definitions. | Pierre-Marie Pédrot |
| 2017-05-25 | Merge PR#406: coq makefile2 | Maxime Dénès |
| 2017-05-23 | add the only target | Enrico Tassi |
| 2017-05-23 | enters coq_makefile2 | Enrico Tassi |
| 2017-05-23 | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias |
| 2017-05-23 | [vernac] Remove `Save.` command. | Emilio Jesus Gallego Arias |
| 2017-05-17 | Documenting relaxing of constraints on injection. | Hugo Herbelin |
| 2017-05-17 | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès |
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-05-11 | Add documentation for Set Ltac Batch Debug | Jason Gross |
| 2017-05-11 | Documenting Printing Compact Contexts + CHANGES | Pierre Courtieu |
| 2017-05-11 | Merge PR#201: Transparent abstract | Maxime Dénès |
| 2017-05-04 | Improve documentation of assert / pose proof / specialize. | Théo Zimmermann |
| 2017-05-03 | Merge PR#411: Mention template polymorphism in the documentation. | Maxime Dénès |
| 2017-05-03 | Fix outdated description in RefMan. | Théo Zimmermann |
| 2017-05-01 | More consistent writing of de Bruijn. | Théo Zimmermann |
| 2017-05-01 | Fix for bug 5507. Mispelt de Bruijn. | Théo Zimmermann |
| 2017-04-28 | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l... | Maxime Dénès |
| 2017-04-27 | fix order of command-line arguments mentioned in Add LoadPath | Paul Steckler |
| 2017-04-25 | Mark transparent_abstract as risky in docs | Jason Gross |
| 2017-04-25 | Add transparent_abstract tactic | Jason Gross |
| 2017-04-24 | refman: remember the old name of template polymorphism. | Gaetan Gilbert |
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r... | Maxime Dénès |
| 2017-04-11 | Update RefMan-pre to mention template polymorphism. | Gaetan Gilbert |
| 2017-04-11 | Use "template polymorphism" in the documentation. | Gaetan Gilbert |
| 2017-04-11 | Mention template polymorphism in the documentation. | Gaetan Gilbert |
| 2017-04-09 | Merge PR#460: Turning the printing primitive projection compatibility flag of... | Maxime Dénès |
| 2017-04-09 | Fixing #5420 as well as many related bugs due to miscounting let-ins. | Hugo Herbelin |
| 2017-04-07 | Merge PR#485: Document Show Match | Maxime Dénès |
| 2017-04-07 | Turning the printing primitive projection parameter flag off by default. | Hugo Herbelin |
| 2017-04-07 | Turning the printing primitive projection compatibility flag off by default. | Hugo Herbelin |
| 2017-04-06 | Merge PR#455: Farewell decl_mode | Maxime Dénès |
| 2017-03-23 | Documenting the grammar {| ... |} syntax for building records. | Hugo Herbelin |
| 2017-03-23 | Merge PR#433: doc: fix a French-ism | Maxime Dénès |
| 2017-03-22 | Fix some typos. | Guillaume Melquiond |
| 2017-03-22 | Merge PR#482: [toplevel] Remove unusable option -notop | Maxime Dénès |
| 2017-03-17 | Document Show Match, add ref to that in match variants/extensions | Paul Steckler |
| 2017-03-14 | doc: fix a French-ism | Valentin Robert |
| 2017-03-14 | [toplevel] Remove unusable option -notop | Emilio Jesus Gallego Arias |
| 2017-03-14 | Merge PR#438: Fix V7 syntax in refman. | Maxime Dénès |
| 2017-03-09 | Typo doc notations. | Hugo Herbelin |