aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/07-commands-and-options
AgeCommit message (Collapse)Author
2020-12-11Clarify changelog categories.Théo Zimmermann
For readers of the changelog: title "Tools" become "Command-line tools". For developers: changelog categories 07 and 08 are disambiguated.
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-11-20Add changelogPierre Roux
2020-11-16Merge PR #13040: [gc] Set GC policy as best-fit in OCaml >= 4.10.0coqbot-app[bot]
Reviewed-by: gares Reviewed-by: ppedrot
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16[gc] Set GC policy as best-fit in OCaml >= 4.10.0Emilio Jesus Gallego Arias
Closes #11277 ; the `space_overhead` parameter has been selected for maximum speedup, in some cases it could also increase memory consumption. Please use `OCAMLRUNPARAM` to tune it and report back your experiments.
2020-11-16Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` ↵Pierre-Marie Pédrot
commands Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-16Document the deprecation of the commands.Pierre-Marie Pédrot
2020-11-16Document the new warning.Pierre-Marie Pédrot
2020-11-15Document the new export locality for the remaining hint commands.Pierre-Marie Pédrot
2020-11-15Merge PR #13339: In -noinit mode, add support for Proof using, using is not ↵Pierre-Marie Pédrot
a keyword. Ack-by: SkySkimmer Reviewed-by: herbelin Ack-by: ppedrot
2020-11-12Add changelog entry for Proof using in -noinit mode.Théo Zimmermann
2020-11-12Move last changelog entry for 8.12.1.Théo Zimmermann
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, ↵coqbot-app[bot]
not only on subidentifiers of an identifier Reviewed-by: Zimmi48
2020-11-12Add changelog for #13345.Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-11Add changelog for #13351.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-06Merge PR #13139: Clean the constr-as-hint APIcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-04Adding change log for #13255.Hugo Herbelin
2020-11-04Document the changes.Pierre-Marie Pédrot
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-17Add changelog.Pierre-Marie Pédrot
2020-07-10Add changelog.Pierre-Marie Pédrot
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 ↵Emilio Jesus Gallego Arias
deprecation. Reviewed-by: Zimmi48 Reviewed-by: ejgallego
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 ↵Pierre-Marie Pédrot
eta-expansion of "match" branches Reviewed-by: gares Ack-by: ppedrot
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
Closes #12351. We set the parameters of the redirect formatter to be same than the ones in stdout. I guess the original semantics was to ignore the parameters, so I'm unsure we want to do this. While we are a it, we include a fix on the formatter, which _must_ be flushed before closing its associated channel.
2020-05-15Changelog entries for #8855.Théo Zimmermann
2020-05-14Merge PR #12296: Fixes #12234: wrong environment for Show ProofGaëtan Gilbert
Reviewed-by: SkySkimmer
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
Reviewed-by: SkySkimmer Ack-by: Zimmi48
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
We deprecate `Hide Obligations` and remove `Shrink Obligations` [deprecated since 8.7]
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
Let vs Definition / Example syntax was split in 7c28130 for parsing reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could be introduced. This split is probably the reason why Let was overlooked when support for universe bindings and universe constraints were added to Definition and variants.
2020-04-02Remove Chapter command.Théo Zimmermann
This was an undocumented equivalent of the Section command.
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-19Document all the existing attributes.Théo Zimmermann
And fix documentation following the removal of the Template Check flag in #11546.
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
Ack-by: herbelin
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-12Add changelogSimonBoulier
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:33:10 +0000