aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/02-specification-language
AgeCommit message (Expand)Author
2021-03-30Remove the :> type castJim Fehrle
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-11-19Add changelog for #13386.Hugo Herbelin
2020-11-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part of...coqbot-app[bot]
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
2020-11-16Changelog for variance syntaxGaëtan Gilbert
2020-11-16Doc for variance syntaxGaëtan Gilbert
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ...coqbot-app[bot]
2020-11-15Add changelog for #13387.Hugo Herbelin
2020-11-15Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an error...coqbot-app[bot]
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handle...coqbot-app[bot]
2020-11-15Add changelog for #13383.Hugo Herbelin
2020-11-15Doc and changelog for Instance Generalized OutputGaëtan Gilbert
2020-11-14Add changelog for #13376.Hugo Herbelin
2020-11-05Adding change log for #13217.Hugo Herbelin
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-11-02add changelogEnrico Tassi
2020-10-31Adding overlay for PR #13290.Hugo Herbelin
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...coqbot-app[bot]
2020-10-16Add change log for #13166.Hugo Herbelin
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
2020-10-05Change log for #12768.Hugo Herbelin
2020-10-05Document the removal of forward class hints.Théo Zimmermann
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-07-23[changelog] Incorporate hanging changelog entry for 8.12+beta1Emilio Jesus Gallego Arias
2020-07-23[changelog] Fix hanging file extension.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:09:08 +0000