| Age | Commit message (Expand) | Author |
| 2017-12-20 | Merge PR #6377: Removal of the FAQ LaTex document. | Maxime Dénès |
| 2017-12-19 | Fix typo in the refman. | Théo Zimmermann |
| 2017-12-18 | Merge PR #6381: A version of [time] that works on constr evaluation | Maxime Dénès |
| 2017-12-18 | Merge PR #6380: Add tactics to reset and display the Ltac profile | Maxime Dénès |
| 2017-12-18 | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra... | Maxime Dénès |
| 2017-12-18 | Removing the FAQ, which has been moved to the GitHub wiki for this | Matt Quinn |
| 2017-12-17 | [doc] Nit on the manual. | Emilio Jesus Gallego Arias |
| 2017-12-15 | Merge PR #6219: Document undocumented options | Maxime Dénès |
| 2017-12-14 | Add documentation for time_constr | Jason Gross |
| 2017-12-14 | Add doc+changelog entries for new LtacProf tactics | Jason Gross |
| 2017-12-14 | Merge PR #978: In printing, experimenting factorizing "match" clauses with sa... | Maxime Dénès |
| 2017-12-14 | Merge PR #6169: Clean up/deprecated options | Maxime Dénès |
| 2017-12-14 | Document Short Module Printing. | Gaëtan Gilbert |
| 2017-12-14 | Document Rewriting Schemes (quickly). | Gaëtan Gilbert |
| 2017-12-14 | Document Record Elimination Schemes. | Gaëtan Gilbert |
| 2017-12-14 | Document Asymmetric Patterns. | Gaëtan Gilbert |
| 2017-12-14 | Document some omega options (missing Omega Oldstyle). | Gaëtan Gilbert |
| 2017-12-14 | Add doc for Set Debug RAKAM. | Gaëtan Gilbert |
| 2017-12-14 | Add doc for Set Debug Cbv. | Gaëtan Gilbert |
| 2017-12-14 | Add doc for Set Info/Debug Auto/Trivial/Eauto. | Gaëtan Gilbert |
| 2017-12-14 | Add optindex for Set Bullet Behavior. | Gaëtan Gilbert |
| 2017-12-14 | Add doc for Set Congruence Verbose | Gaëtan Gilbert |
| 2017-12-14 | Fix typo in doc optindex for Typeclass Resolution ... | Gaëtan Gilbert |
| 2017-12-12 | Documenting the new options for printing "match". | Hugo Herbelin |
| 2017-12-11 | Remove deprecated appcontext and corresponding documentation. | Théo Zimmermann |
| 2017-12-10 | [make] remove unneeded generated file "tolink.ml" | Emilio Jesus Gallego Arias |
| 2017-12-10 | [build] Remove coqmktop in favor of ocamlfind. | Emilio Jesus Gallego Arias |
| 2017-12-07 | Merge PR #6277: Qualified import in coqchk | Maxime Dénès |
| 2017-12-05 | use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language | Paul Steckler |
| 2017-12-05 | Merge PR #890: Global universe declarations | Maxime Dénès |
| 2017-12-05 | Merge PR #6300: Clarify operation of sequences, fixes #6095 | Maxime Dénès |
| 2017-12-05 | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 | Maxime Dénès |
| 2017-12-01 | clarify operation of sequences, #6095 | Paul Steckler |
| 2017-12-01 | [refman] Expand a little on global universes. | Matthieu Sozeau |
| 2017-12-01 | Documenting the -Q flag of coqchk. | Pierre-Marie Pédrot |
| 2017-12-01 | Merge PR #6276: Coqchk accepts filenames | Maxime Dénès |
| 2017-11-29 | Documenting the possibility to pass filenames to coqchk. | Pierre-Marie Pédrot |
| 2017-11-28 | use \ocaml macro in new text | Paul Steckler |
| 2017-11-28 | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | Gaëtan Gilbert |
| 2017-11-28 | Merge PR #1033: Universe binder improvements | Maxime Dénès |
| 2017-11-25 | Updating the current official writing of OCaml, updating Camlp4->Camlp5. | Hugo Herbelin |
| 2017-11-25 | Allow local universe renaming in Print. | Gaëtan Gilbert |
| 2017-11-22 | use OCaml criteria for infix ops, #6212 | Paul Steckler |
| 2017-11-19 | Rename coq-inferior.el -> inferior-coq.el to match provided feature. | Gaëtan Gilbert |
| 2017-11-13 | coq_makefile: document COQ_SRC_SUBDIRS | Enrico Tassi |
| 2017-11-06 | Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]", | Samuel Gruetter |
| 2017-11-06 | Merge PR #1139: Add a linter. | Maxime Dénès |
| 2017-10-27 | Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631 | Maxime Dénès |
| 2017-10-25 | Rename \Tree to \NatTree | Johannes Kloos |
| 2017-10-25 | Put newlines at the end of files. | Gaëtan Gilbert |