| Age | Commit message (Expand) | Author |
|---|
| 2021-04-02 | Remove the omega tactic and related options | Jim Fehrle |
| 2021-03-08 | Convert 2nd part of rewriting chapter to prodn | Jim Fehrle |
| 2021-01-07 | Use nat_or_var for fail/gfail | Jim Fehrle |
| 2020-12-30 | Convert rewriting and proof-mode chapters to prodn | Jim Fehrle |
| 2020-11-24 | Convert auto chapter to prodn | Jim Fehrle |
| 2020-11-20 | Use nat_or_var where negative values don't make sense | Jim Fehrle |
| 2020-11-10 | Convert logic.rst to prodn | Jim Fehrle |
| 2020-11-09 | Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml... | coqbot-app[bot] |
| 2020-11-09 | [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. | Théo Zimmermann |
| 2020-11-09 | Fix #5226: Add index entry for ::=. | Théo Zimmermann |
| 2020-11-09 | Fix indentation of todo in Ltac chapter. | Théo Zimmermann |
| 2020-10-27 | Rename misc nonterminals | Jim Fehrle |
| 2020-10-24 | Convert misc chapters to prodn | Jim Fehrle |
| 2020-10-20 | Add some missing smallcaps. | Théo Zimmermann |
| 2020-09-11 | Turn integer into natural in several mlgs | Pierre Roux |
| 2020-09-11 | [refman] Rename int to integer | Pierre Roux |
| 2020-09-11 | [refman] Rename num to natural | Pierre Roux |
| 2020-09-07 | Explain how selectors change the order of goals | Jim Fehrle |
| 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-14 | Reintroduce leftover parts; update index files; small fixes. | Théo Zimmermann |
| 2020-05-06 | Moving lazymatch and multimatch to simple identifiers. | Hugo Herbelin |
| 2020-05-06 | Mention keywords from g_ltac.mlg used in Ltac. | Hugo Herbelin |
| 2020-05-03 | Merge PR #12197: LtacProf now handles multi-success backtracking | Pierre-Marie Pédrot |
| 2020-05-02 | LtacProf now handles multi-success backtracking | Jason Gross |
| 2020-05-01 | Move essential vocabulary and syntax conventions to section on basics. | Théo Zimmermann |
| 2020-04-26 | Convert syntax extensions chapter to prodn | Jim Fehrle |
| 2020-04-17 | Deprecate “omega” | Vincent Laporte |
| 2020-04-10 | Convert vernac commands chapter to prodn, update syntax | Jim Fehrle |
| 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-10-29 | Fix #9114, assert_succeeds (exact I) solves goal | Jason Gross |
| 2019-10-29 | `assert_succeeds`&`assert_fails`: multisuccess fix | Jason Gross |
| 2019-10-22 | documentation fixes | Antonio Nikishaev |
| 2019-07-28 | Update documentation on tokens, use "int" and "num" | Jim Fehrle |
| 2019-06-15 | Rename expr and tacexpr tokens into ltac_expr token family. | Théo Zimmermann |
| 2019-05-23 | Define many undefined tokens, and other misc fixes. | Théo Zimmermann |
| 2019-05-22 | [refman] Add more missing @ signs | Clément Pit-Claudel |
| 2019-05-22 | [refman] Misc fixes (mostly missing '@' signs) | Clément Pit-Claudel |
| 2019-05-21 | Fixing typos - Part 1 | JPR |
| 2019-05-19 | [refman] Misc fixes (indentation, whitespace, notation syntax) | Clément Pit-Claudel |
| 2019-05-10 | Better title for the first example of the Ltac examples section. | Théo Zimmermann |
| 2019-05-09 | Improve the first two Ltac examples. | Théo Zimmermann |
| 2019-05-09 | Rewording, language improvements. | Théo Zimmermann |
| 2019-05-08 | [refman] Move all the Ltac examples to the Ltac chapter. | Théo Zimmermann |
| 2019-05-07 | Integrate build and documentation of Ltac2 | Maxime Dénès |
| 2019-03-27 | [doc] [abstract] Document a bit some problems with abstract. | Emilio Jesus Gallego Arias |
| 2019-03-08 | [sphinx] Fix typo in local application of tactics | hawnzug |
| 2019-02-18 | Using options abort and restart of coqtop directive in the manual. | Théo Zimmermann |
| 2019-02-18 | Sphinx: fail when a command fails | Gaëtan Gilbert |
