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