| Age | Commit message (Expand) | Author |
|---|
| 2017-06-26 | Merge PR#756: Fix Bug #5574, document function scope | Maxime Dénès |
| 2017-06-23 | Fix Bug #5574, document function scope | Paul Steckler |
| 2017-06-23 | Merge PR#740: Refactor documentation of records. | Maxime Dénès |
| 2017-06-19 | Merge PR#777: Improving documentation of tactic "move" (report #4561) | Maxime Dénès |
| 2017-06-16 | Refactor documentation of records. | Théo Zimmermann |
| 2017-06-16 | Merge PR#767: Document named evars (including Show ident) | Maxime Dénès |
| 2017-06-16 | Document cumulativity for inductive types | Amin Timany |
| 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-13 | Merge remote-tracking branch 'upstream/trunk' into trunk | William Lawvere |
| 2017-06-14 | Remove support for Coq 8.4. | Guillaume Melquiond |
| 2017-06-13 | doc: improve grammar of RefMan-syn | William Lawvere |
| 2017-06-13 | Improving documentation of tactic "move" (report #4561). | Hugo Herbelin |
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey |
| 2017-06-13 | Document instantiate (ident := term) and make it the preferred variant. | Théo Zimmermann |
| 2017-06-13 | Document Show ident. | Théo Zimmermann |
| 2017-06-13 | Document evar naming syntax. | Théo Zimmermann |
| 2017-06-12 | Remove commented documentation for Show Tree. | Théo Zimmermann |
| 2017-06-07 | Fix documentation of Typeclasses eauto := | 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 |
