| Age | Commit message (Expand) | Author |
|---|
| 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 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 |
| 2019-06-05 | Changelog entry for Ltac2 (missing from #10002). | Théo Zimmermann |
| 2019-06-05 | Fix #10283: clearer dependency documentation for building CoqIDE. | Théo Zimmermann |
| 2019-06-04 | Fix typo in changelog | Enrico Tassi |
| 2019-06-04 | [rewrite] Add Morphism syntax made different for module type parameters | Enrico Tassi |
| 2019-06-04 | [function] always open a proof when used with `wf` or `measure` | Enrico Tassi |
| 2019-06-04 | coqpp: add new ![] specifiers for structured proof interaction | Gaëtan Gilbert |
| 2019-06-04 | Proof_global: pass only 1 pstate when we don't want the proof stack | Gaëtan Gilbert |
| 2019-06-03 | Merge PR #10287: Update tutorial plugin to use sigma instad of evd, in keepin... | Enrico Tassi |
| 2019-06-03 | Merge PR #10277: Remove Show Script (deprecated in 8.10) | Théo Zimmermann |
| 2019-06-03 | Merge PR #10261: Update doc to reflect that PG now supports Coq-generated pro... | Théo Zimmermann |
| 2019-06-03 | Update tutorial plugin to use sigma, in keeping with doc recommendations | Talia Ringer |
| 2019-06-03 | Update doc to reflect that PG now supports Coq-generated proof diffs | Jim Fehrle |
| 2019-05-31 | Remove Show Script (deprecated in 8.10) | Gaëtan Gilbert |
| 2019-05-28 | [elaboration] Bidirectionality hints | Maxime Dénès |
| 2019-05-26 | Merge PR #10220: Use new coqrst syntax for alternatives in SSReflect chapter. | Enrico Tassi |
| 2019-05-25 | Documenting syntax "injection ... as [= pat1 ... patn ]". | Hugo Herbelin |
| 2019-05-24 | Remove the indirect opaque accessor hooks from Opaqueproof. | Pierre-Marie Pédrot |
| 2019-05-23 | Merge PR #10118: Make progress toward #9411: reject new undefined references. | Clément Pit-Claudel |
| 2019-05-24 | Merge PR #10167: do not parse `|` as infix in patterns; parse `|}` as `|` `}` | Emilio Jesus Gallego Arias |
| 2019-05-23 | Make progress toward #9411: reject new undefined references. | Théo Zimmermann |
| 2019-05-23 | Merge PR #10195: Minor Ltac2 documentation fix: type parameters are optional. | Clément Pit-Claudel |
| 2019-05-23 | Merge PR #10217: Less undefined tokens | Clément Pit-Claudel |
| 2019-05-23 | do not parse `|` as infix in patterns; parse `|}` as `|` `}` | Georges Gonthier |
| 2019-05-23 | Suggestions from review. | Théo Zimmermann |
| 2019-05-23 | Update doc/sphinx/user-extensions/syntax-extensions.rst | Maxime Dénès |
| 2019-05-23 | Update doc/sphinx/user-extensions/syntax-extensions.rst | Maxime Dénès |
| 2019-05-23 | Update doc/sphinx/user-extensions/syntax-extensions.rst | Maxime Dénès |
| 2019-05-23 | More misc refman fixes, less undefined tokens. | Théo Zimmermann |
