aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/07-commands-and-options
AgeCommit message (Expand)Author
2020-06-05Add remaining 8.12+beta1 changelog entries.Théo Zimmermann
2020-06-02Merge PR #11974: Require in Section: warning is now about fragility not depre...Emilio Jesus Gallego Arias
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...Pierre-Marie Pédrot
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
2020-05-15Changelog entries for #8855.Théo Zimmermann
2020-05-14Merge PR #12296: Fixes #12234: wrong environment for Show ProofGaëtan Gilbert
2020-05-14Add a changelog for 8.11.2.Pierre-Marie Pédrot
2020-05-14Added change log.Hugo Herbelin
2020-05-13Added change log.Hugo Herbelin
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-15Ignore -native-compiler option when disabledPierre Roux
2020-04-10[obligations] Deprecated flag cleanupEmilio Jesus Gallego Arias
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
2020-04-02Remove Chapter command.Théo Zimmermann
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-19Document all the existing attributes.Théo Zimmermann
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-12Add changelogSimonBoulier
2020-03-08Minor improvements to the unreleased changelog.Théo Zimmermann
2020-02-28Deprecating the declaration of arbitrary terms as hints.Pierre-Marie Pédrot
2020-02-23Remove unqualified universe attributes.Théo Zimmermann
2020-02-20[init] Add `-boot` option to avoid binding `Coq.` prefix.Emilio Jesus Gallego Arias
2020-02-13Merge PR #11441: Add explicit types to changelog entries that were still miss...Emilio Jesus Gallego Arias
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
2020-01-22Add explicit types to changelog entries.Théo Zimmermann
2020-01-22Move new entries in 8.11.0 changelog.Théo Zimmermann
2020-01-20[mltop] Deprecate -load-ml options in anticipation of #11409Emilio Jesus Gallego Arias
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-24[CS] Allow a variable introduced with Let to be a canonical instanceEnrico Tassi
2019-12-20Coherence checking for coercionsKazuhiko Sakaguchi
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-02Move unreleased changelog to new 8.11 section.Théo Zimmermann
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-28[changelog] Add types to changelog entries.Théo Zimmermann
2019-11-27Changelog entry for #11187.Théo Zimmermann
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-17Add changelog entryMaxime Dénès
2019-09-12Release notes for 8.10+beta3.Théo Zimmermann
2019-08-16Add documentation for typing flags.SimonBoulier
2019-07-04Fix miscellaneous mistakes in unreleased changelog entries.Théo Zimmermann
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ...Kazuhiko Sakaguchi
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 03:37:00 +0000