| Age | Commit message (Expand) | Author |
|---|
| 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-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 |
| 2016-06-16 | Revise syntax of Hint Cut | Matthieu Sozeau |
| 2016-06-14 | Add documentation for goal selectors. | Cyprien Mangin |
| 2016-05-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-05-03 | In Regular Subst Tactic mode, ensure that the order of hypotheses is | Hugo Herbelin |
| 2016-03-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-02-24 | Document Hint Mode, cleanup Hint doc. | Matthieu Sozeau |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Clarifying the documentation of tactics "cbv" and "lazy". | Hugo Herbelin |
| 2016-01-14 | Updating and improving the documentation of intros patterns. | Hugo Herbelin |
| 2016-01-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-12 | Documenting dtauto and dintuition. | Hugo Herbelin |
| 2016-01-12 | Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding". | Hugo Herbelin |
| 2016-01-12 | Documenting option 'Set Bracketing Last Introduction Pattern'. | Hugo Herbelin |
| 2016-01-12 | restore documentation of admit | Enrico Tassi |
