| Age | Commit message (Expand) | Author |
| 2017-10-24 | Fix #4846 | Johannes Kloos |
| 2017-10-24 | Fix #5413: [unfold ... in] not documented | Johannes Kloos |
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond |
| 2017-09-01 | add option index entry for NativeCompute Profiling | Paul Steckler |
| 2017-08-18 | use OCaml temp_file, instead of our own version | Paul Steckler |
| 2017-08-17 | Add native compute profiling, BZ#5170 | Paul Steckler |
| 2017-08-16 | mention that tactic is the identity or gives error | Paul Steckler |
| 2017-08-16 | change section caption, improve some wording | Paul Steckler |
| 2017-07-28 | Fix documentation of Hint Mode (bug #4911). | Guillaume Melquiond |
| 2017-07-11 | Sync the manual with the deprecation warnings. | Théo Zimmermann |
| 2017-07-05 | Merge PR #837: Add inversion_sigma to CHANGES and to doc | Maxime Dénès |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-06-30 | Add doc for inversion_sigma to RefMan-tac | Jason Gross |
| 2017-06-19 | Merge PR#777: Improving documentation of tactic "move" (report #4561) | Maxime Dénès |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey |
| 2017-06-13 | Improving documentation of tactic "move" (report #4561). | Hugo Herbelin |
| 2017-06-13 | Document instantiate (ident := term) and make it the preferred variant. | 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-17 | Documenting relaxing of constraints on injection. | Hugo Herbelin |
| 2017-05-04 | Improve documentation of assert / pose proof / specialize. | Théo Zimmermann |
| 2017-04-09 | Fixing #5420 as well as many related bugs due to miscounting let-ins. | Hugo Herbelin |
| 2016-12-06 | Fix broken documentation in presence of \zeroone{... \tt ...}. | Guillaume Melquiond |
| 2016-12-06 | Update documentation (bugs #5246 and #5251). | Guillaume Melquiond |
| 2016-11-08 | Merge remote-tracking branch 'github/pr/348' into v8.6 | Maxime Dénès |
| 2016-11-07 | Merge remote-tracking branch 'github/pr/339' into v8.6 | Maxime Dénès |
| 2016-11-07 | Document two new variants of refine | Matthieu Sozeau |
| 2016-11-05 | Minor fix in documentation | Matthieu Sozeau |
| 2016-11-04 | Merge remote-tracking branch 'github/pr/336' into v8.6 | Maxime Dénès |
| 2016-11-03 | Lets Hints/Instances take an optional pattern | Matthieu Sozeau |
| 2016-10-29 | Documenting changes in typeclasses | Matthieu Sozeau |
| 2016-10-25 | Remove v62 from the refman. | Théo Zimmermann |
| 2016-10-24 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot |
| 2016-10-19 | Documenting Hint Resolve -> and <- variants. | Théo Zimmermann |
| 2016-10-19 | Making the doc of auto hints more precise. | Théo Zimmermann |
| 2016-10-18 | Extending the doc with a general summary of auto variants. | Théo Zimmermann |
| 2016-10-18 | Document info_auto. | Théo Zimmermann |
| 2016-10-18 | Improve the documentation of eauto. | Théo Zimmermann |
| 2016-10-03 | fixing bug 4609: document an option governing the generation of equalities | Yves Bertot |
| 2016-09-30 | Merge branch 'v8.5' into v8.6 | Maxime Dénès |
| 2016-09-28 | Merge remote-tracking branch 'github/pr/232' into v8.6 | Maxime Dénès |
| 2016-09-27 | Fixing #4887 (confusion between using and with in documentation of firstorder). | Hugo Herbelin |
| 2016-09-15 | Extending "contradiction" so that it recognizes statements such as "~x=x" or ... | Hugo Herbelin |
| 2016-09-12 | Refolding: disable in 8.4 compat file, document | Matthieu Sozeau |
| 2016-08-21 | Documenting "Set Structural Injection". | Hugo Herbelin |
| 2016-07-01 | Add and document match, fix and cofix reduction flags. | Maxime Dénès |
| 2016-06-30 | Update the documentation for goal selectors. | Cyprien Mangin |
| 2016-06-29 | Updated CHANGES about subst. More on recursive equations in reference manual. | Hugo Herbelin |
| 2016-06-16 | Document new Hint Mode option. | Matthieu Sozeau |