| Age | Commit message (Expand) | Author |
| 2021-03-08 | Convert 2nd part of rewriting chapter to prodn | Jim Fehrle |
| 2021-02-24 | Infrastructure for fine-grained debug flags | Maxime Dénès |
| 2021-02-08 | Properly document the local and global locality attributes. | Théo Zimmermann |
| 2021-01-25 | Remove the SearchHead command | Jim Fehrle |
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle |
| 2020-11-26 | [attributes] [typing] Rename `typing` to `bypass_check` | Emilio Jesus Gallego Arias |
| 2020-11-26 | [attributes] [doc] Documentation review by Théo. | Emilio Jesus Gallego Arias |
| 2020-11-26 | [vernac] Allow to control typing flags with attributes. | Emilio Jesus Gallego Arias |
| 2020-11-24 | Convert auto chapter to prodn | Jim Fehrle |
| 2020-11-14 | Distinguish one_pattern and one_term nonterminals | Jim Fehrle |
| 2020-11-12 | Clarifying the role of Add ML Path vs -I (see #13344). | Hugo Herbelin |
| 2020-11-09 | [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. | Théo Zimmermann |
| 2020-11-05 | Various fixes. | Théo Zimmermann |
| 2020-10-24 | Convert misc chapters to prodn | Jim Fehrle |
| 2020-10-20 | Add some missing smallcaps. | Théo Zimmermann |
| 2020-09-11 | [refman] Rename int to integer | Pierre Roux |
| 2020-09-11 | [refman] Rename num to natural | Pierre Roux |
| 2020-08-25 | Convert ltac2 chapter to use prodn, update syntax | Jim Fehrle |
| 2020-06-08 | Convert Ltac chapter to prodn | Jim Fehrle |
| 2020-05-16 | Merge PR #8855: More search options | Emilio Jesus Gallego Arias |
| 2020-05-15 | Document new Search features. | Théo Zimmermann |
| 2020-05-14 | Add some markers of origin. | Théo Zimmermann |
| 2020-05-14 | Reintroduce leftover parts; update index files; small fixes. | Théo Zimmermann |
| 2020-05-09 | Add a `with_strategy` tactic | Jason Gross |
| 2020-05-01 | Remove flags, options and tables from vernac chapter. | Théo Zimmermann |
| 2020-04-28 | Merge PR #11718: Convert syntax extensions chapter to prodn | Théo Zimmermann |
| 2020-04-26 | Convert syntax extensions chapter to prodn | Jim Fehrle |
| 2020-04-23 | Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line... | Pierre-Marie Pédrot |
| 2020-04-21 | Document changed warnings and erros following #12038. | Théo Zimmermann |
| 2020-04-16 | Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative | Gaëtan Gilbert |
| 2020-04-11 | Merge PR #11961: Convert vernac commands chapter to prodn, update syntax | Théo Zimmermann |
| 2020-04-10 | Convert vernac commands chapter to prodn, update syntax | Jim Fehrle |
| 2020-04-07 | Fix documentation of Print Libraries following #10476. | Théo Zimmermann |
| 2020-03-29 | Merge PR #11944: Remove SearchAbout command, deprecated in 8.5 | Théo Zimmermann |
| 2020-03-28 | Remove SearchAbout command, deprecated in 8.5 | Jim Fehrle |
| 2020-03-28 | Document change of behavior of Fail in 8.11. | Théo Zimmermann |
| 2020-03-25 | Convert Gallina Extensions to use prodn | Jim Fehrle |
| 2020-03-19 | Interpret the Export modifier of Set and Unset as an attribute. | Théo Zimmermann |
| 2020-03-19 | Document all the existing attributes. | Théo Zimmermann |
| 2020-03-18 | Add documentation for the export hint. | Pierre-Marie Pédrot |
| 2020-03-03 | [loadpath] Rework and simplify ML loadpath handling | Emilio Jesus Gallego Arias |
| 2020-01-10 | missing space | Olivier Laurent |
| 2019-11-20 | Update grammar in the Terms section of Gallina chapter | Jim Fehrle |
| 2019-11-06 | Replace "option" in doc when it refers to a flag | Jim Fehrle |
| 2019-09-19 | Fix #10420 Add dependent evar mapping info to output | Jim Fehrle |
| 2019-09-03 | Add missing index for From ... Require ... | Théo Zimmermann |
| 2019-08-16 | Universe Checking instead of Universes Checking | SimonBoulier |
| 2019-08-16 | Add documentation for typing flags. | SimonBoulier |
| 2019-07-25 | Remove deprecated `Backtrack` command | Maxime Dénès |
| 2019-05-23 | Suggestions from review. | Théo Zimmermann |