aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...Pierre-Marie Pédrot
2019-06-08Updated changelog.Hugo Herbelin
2019-06-07Merge PR #10311: Ltac2 codeowner / changelogMaxime Dénès
2019-06-07Update changelog for 103032 and 10305Enrico Tassi
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-05Changelog entry for Ltac2 (missing from #10002).Théo Zimmermann
2019-06-04Fix typo in changelogEnrico Tassi
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-03Merge PR #10277: Remove Show Script (deprecated in 8.10)Théo Zimmermann
2019-06-03Merge PR #10261: Update doc to reflect that PG now supports Coq-generated pro...Théo Zimmermann
2019-06-03Update doc to reflect that PG now supports Coq-generated proof diffsJim Fehrle
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-13Move last changelog entries for 8.10+beta1.Théo Zimmermann
2019-05-13Merge PR #10085: Do not include unreleased changelog in released versions.Vincent Laporte
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to p...Enrico Tassi
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10Changelog for PR #10076Vincent Laporte
2019-05-08Update release process documentation and changelog entry.Théo Zimmermann
2019-05-05Add changelog entry about moving changelog to refman.Théo Zimmermann
2019-05-05Create categories in changelog.Théo Zimmermann
2019-05-05New infrastructure for the unreleased changelog.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-03 22:31:27 +0000