| Age | Commit message (Expand) | Author |
| 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-15 | Merge PR #6429: 8.7.1 CHANGES. | 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 | 8.7.1 CHANGES. | Théo Zimmermann |
| 2017-12-12 | In printing, factorizing "match" clauses with same right-hand side. | Hugo Herbelin |
| 2017-12-07 | Merge PR #873: New strategy based on open scopes for deciding which notation ... | Maxime Dénès |
| 2017-12-05 | use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language | Paul Steckler |
| 2017-12-01 | Update CHANGES | Matthieu Sozeau |
| 2017-12-01 | Merge PR #6276: Coqchk accepts filenames | Maxime Dénès |
| 2017-11-29 | Remove "obsolete_locality" and fix STM vernac classification. | Maxime Dénès |
| 2017-11-29 | Documenting the possibility to pass filenames to coqchk. | Pierre-Marie Pédrot |
| 2017-11-27 | Selecting which notation to print based on current stack of scope. | Hugo Herbelin |
| 2017-10-26 | Passing around the flag for injection so that tactics calling inj at | Hugo Herbelin |
| 2017-10-19 | Moving bug numbers to BZ# format in the CHANGES file. | Théo Zimmermann |
| 2017-10-10 | Merge PR #540: [configure] Support for flambda flags. | Maxime Dénès |
| 2017-10-10 | Merge PR #768: Omega and romega know about context definitions (fix old bug 148) | Maxime Dénès |
| 2017-10-10 | [configure] Support for flambda flags. | Emilio Jesus Gallego Arias |
| 2017-10-09 | Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on... | Maxime Dénès |
| 2017-10-06 | 8.7+beta2 CHANGES | Théo Zimmermann |
| 2017-10-05 | romega: takes advantage of context variables with body | Pierre Letouzey |
| 2017-10-05 | Omega now aware of context variables with bodies (in type Z or nat) (fix bug ... | Pierre Letouzey |
| 2017-10-02 | Mention requiring extraction/funind in CHANGES | Tej Chajed |
| 2017-09-25 | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler |
| 2017-09-15 | Fix CHANGES after merge of PR #1025. | Théo Zimmermann |
| 2017-09-05 | read flags from project file for Compile Buffer | Paul Steckler |
| 2017-09-01 | move mention of native_compute profiling in CHANGES | Paul Steckler |
| 2017-08-29 | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès |
| 2017-08-18 | add CHANGES entry | Paul Steckler |
| 2017-08-18 | Correct the option for cumulativity in CHANGES | Amin Timany |
| 2017-08-17 | Use the wording suggested by Gaetan. | Théo Zimmermann |
| 2017-08-17 | Addition suggested by Pierre-Marie. | Théo Zimmermann |
| 2017-08-16 | Additions following Hugo's suggestions. | Théo Zimmermann |
| 2017-08-16 | Improve wording. | Théo Zimmermann |
| 2017-08-16 | 8.7 CHANGES | Théo Zimmermann |
| 2017-08-16 | Porting #856 (8.6.1 CHANGES entries) to master | Théo Zimmermann |
| 2017-08-01 | Merge PR #925: Document Extraction TestCompile | Maxime Dénès |
| 2017-07-27 | Extraction TestCompile documented + mentionned in CHANGES | Pierre Letouzey |
| 2017-07-26 | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin |
| 2017-07-11 | Add an entry to CHANGES about timing in coq_makefile | Jason Gross |
| 2017-06-30 | Update CHANGES with inversion_sigma entry | Jason Gross |
| 2017-06-20 | Merge PR#774: [ide] Add route_id parameter to query call. | Maxime Dénès |
| 2017-06-18 | [ide] Add route_id parameter to query call. | Emilio Jesus Gallego Arias |
| 2017-06-16 | Document cumulativity for inductive types | Amin Timany |
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey |
| 2017-06-12 | Merge PR#709: Bytecode compilation apart from 'make world', again | Maxime Dénès |
| 2017-06-01 | mention 'make world' without 'byte' in CHANGES + 2 minor suggestions | Pierre Letouzey |