| Age | Commit message (Expand) | Author |
|---|
| 2019-07-01 | Update doc for % escapes in Sphinx doc, improve error messages | Jim Fehrle |
| 2019-06-30 | Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG. | Emilio Jesus Gallego Arias |
| 2019-06-25 | Re-add the "Show Goal" command for Prooftree in PG. | Jim Fehrle |
| 2019-06-25 | Give a functional type to Ltac1 quotations with a context. | Pierre-Marie Pédrot |
| 2019-06-25 | Documenting the Ltac2 change. | Pierre-Marie Pédrot |
| 2019-06-24 | [api] Move `locality` from `library` to `vernac`. | Emilio Jesus Gallego Arias |
| 2019-06-24 | [lemmas] [proof] Split proof kinds into per-layer components. | Emilio Jesus Gallego Arias |
| 2019-06-19 | Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations i... | Théo Zimmermann |
| 2019-06-17 | Merge PR #10392: Fix the changelog of 8.10+beta2 following the backport of #1... | Clément Pit-Claudel |
| 2019-06-17 | Merge PR #10362: Kernel-side delaying of polymorphic opaque constants | Gaëtan Gilbert |
| 2019-06-17 | Fix the changelog of 8.10+beta2 following the backport of #10205. | Théo Zimmermann |
| 2019-06-17 | Update copyright years outside of headers. | Théo Zimmermann |
| 2019-06-17 | Adapt change-header script to handle shebangs in addition to Emacs comments. | Théo Zimmermann |
| 2019-06-17 | Update py-style headers to new year. | Théo Zimmermann |
| 2019-06-17 | Update c-style headers to new year. | Théo Zimmermann |
| 2019-06-17 | Allow to delay polymorphic opaque constants. | Pierre-Marie Pédrot |
| 2019-06-17 | Merge PR #10368: Update, expand, and document plugin tutorial 2 | Enrico Tassi |
| 2019-06-16 | Changelog for 8.10+beta2. | Théo Zimmermann |
| 2019-06-16 | Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern". | Hugo Herbelin |
| 2019-06-15 | Merge PR #10377: Rename expr and tacexpr tokens into ltac_expr token family. | Clément Pit-Claudel |
| 2019-06-15 | Rename expr and tacexpr tokens into ltac_expr token family. | Théo Zimmermann |
| 2019-06-14 | Merge PR #10376: Add a comment documenting what fontsupport.py is. | Clément Pit-Claudel |
| 2019-06-14 | Add a comment documenting what fontsupport.py is. | Théo Zimmermann |
| 2019-06-14 | Merge PR #10322: Update changes.rst as a follow-up to #9743 | Théo Zimmermann |
| 2019-06-13 | Merge PR #10374: Integrate 8.9.0 and 8.9.1 changelog entries. | Clément Pit-Claudel |
| 2019-06-13 | Integrate 8.9.0 and 8.9.1 changelog entries. | Théo Zimmermann |
| 2019-06-13 | Add missing changelog entry for #10360. | Théo Zimmermann |
| 2019-06-13 | Update, expand, and document plugin tutorial 2 | Talia Ringer |
| 2019-06-12 | Merge PR #10310: Fix #10283: clearer dependency documentation for building Co... | Clément Pit-Claudel |
| 2019-06-12 | Merge PR #10329: Update changelog for 10302 and 10305 | Théo Zimmermann |
| 2019-06-12 | Merge PR #10180: `deprecated` attribute support for notations and syntactic d... | Théo Zimmermann |
| 2019-06-09 | [proof] Move proofs that have an associated constant to `Lemmas` | Emilio Jesus Gallego Arias |
| 2019-06-09 | Merge PR #8726: More robust treatment of the Discharge status | Pierre-Marie Pédrot |
| 2019-06-09 | Merge PR #10245: Command line: adding variants for Require, aligning on the v... | Emilio Jesus Gallego Arias |
| 2019-06-08 | Cleaning the status of Local Definition and similar. | Hugo Herbelin |
| 2019-06-08 | Test goal range in "only" selectors | Gaëtan Gilbert |
| 2019-06-08 | Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ... | Pierre-Marie Pédrot |
| 2019-06-08 | Updated changelog. | Hugo Herbelin |
| 2019-06-08 | Mini fix documentation coqtop in passing. | Hugo Herbelin |
| 2019-06-08 | Documenting new options -require-import, -require-export, etc. | Hugo Herbelin |
| 2019-06-07 | Merge PR #10311: Ltac2 codeowner / changelog | Maxime Dénès |
| 2019-06-07 | Update changelog for 103032 and 10305 | Enrico Tassi |
| 2019-06-07 | Merge PR #10205: Make discriminate tactic compatible with HoTT | Pierre-Marie Pédrot |
| 2019-06-06 | Update doc/changelog/03-notations/10180-deprecate-notations.rst | Maxime Dénès |
| 2019-06-06 | Make discriminate tactic compatible with HoTT | Andreas Lynge |
| 2019-06-06 | Update changes.rst as a follow-up to #9743 | Kazuhiko Sakaguchi |
| 2019-06-06 | Update doc/changelog/03-notations/10180-deprecate-notations.rst | Maxime Dénès |
| 2019-06-06 | Clean, document, and expand plugin tutorials 0 and 1 | Talia Ringer |
| 2019-06-06 | [Ltac2] Interpretation scopes in “constr” arguments of tactic notations | Vincent Laporte |
| 2019-06-06 | `deprecated` attribute support for notations and syntactic definitions | Maxime Dénès |
