aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/02-specification-language
AgeCommit message (Expand)Author
2020-06-05Add remaining 8.12+beta1 changelog entries.Théo Zimmermann
2020-06-01Merge PR #12396: Release notes 8.12Emilio Jesus Gallego Arias
2020-05-29Change log for #12422.Hugo Herbelin
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-14Add changelog for #12323.Hugo Herbelin
2020-05-02Adding change logs for PR #12121.Hugo Herbelin
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-03-31Include review suggestionsGaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-14Merge PR #10858: Implementing postponed constraints in TC resolutionGaëtan Gilbert
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-08Minor improvements to the unreleased changelog.Théo Zimmermann
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
2020-02-11Lately adding a changelog for PR#10202.Hugo Herbelin
2020-02-04Non maximal implicits: entry in dev/doc/changes.mdSimonBoulier
2020-02-04Add changelog for non maximal implicit argsSimonBoulier
2020-01-22Changelog for 8.11.0.Théo Zimmermann
2020-01-08Update doc/changelog/02-specification-language/11368-trailing_implicit_error.rstSimonBoulier
2020-01-07Trailing implicit error: changelogSimonBoulier
2019-12-30Merge PR #11233: Fixes #11231: missing dependency in looking for default clau...Pierre-Marie Pédrot
2019-12-12restrict minimization to set to flexiblesGaëtan Gilbert
2019-12-04Update doc/changelog/02-specification-language/11233-master+fix11231-missing-...Hugo Herbelin
2019-12-03Fixes #11231 (missing dependency in pattern-matching decompilation).Hugo Herbelin
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-11-28[changelog] Add types to changelog entries.Théo Zimmermann
2019-11-21Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fi...Emilio Jesus Gallego Arias
2019-11-21Update doc/changelog/02-specification-language/11132-master+fix-implicit-let-...Hugo Herbelin
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-10-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
2019-10-31changelog for #10985Gaëtan Gilbert
2019-10-30Implement the unsupported attribute error using the warning systemGaëtan Gilbert
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
2019-07-18Adding changelog and documentation.Pierre-Marie Pédrot
2019-07-04Fix miscellaneous mistakes in unreleased changelog entries.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-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-10Changelog for PR #10076Vincent Laporte
2019-05-05Create categories in changelog.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 02:46:43 +0000