aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
2021-02-25Merge PR #13202: Infrastructure for fine-grained debug flagscoqbot-app[bot]
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-22changelog for 8.13.1Enrico Tassi
2021-02-20Update doc/changelog/01-kernel/13867-changelog-for-13867.rstEnrico Tassi
2021-02-20add changelog for 13867Enrico Tassi
2021-02-09Merge PR #13822: Remove deprecated command line argumentscoqbot-app[bot]
2021-02-04Changelog for #13822Gaëtan Gilbert
2021-02-01Add changelog entryslrnsc
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
2021-01-28Merge PR #13763: Remove the SearchHead command (deprecated in 8.12)coqbot-app[bot]
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
2021-01-25Remove the SearchHead commandJim Fehrle
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-25Update doc/changelog/04-tactics/13781-deprecate_micromega_options.rstFrédéric Besson
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
2021-01-22changelogBESSON Frederic
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
2021-01-20Remove double induction tacticJim Fehrle
2021-01-19Remove Add InjTyp and 10 other micromega commandsJim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction pat...Pierre-Marie Pédrot
2021-01-18Adding changelog for #13512.Hugo Herbelin
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2021-01-18Add changelogPierre Roux
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ...Pierre-Marie Pédrot
2021-01-07Merge PR #13715: [micromega] Add missing support for `implb`Vincent Laporte
2021-01-06Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-m...coqbot-app[bot]
2021-01-06[micromega] Add missing support for `implb`BESSON Frederic
2021-01-04Document the change of case representation.Pierre-Marie Pédrot
2021-01-04Changelog for 8.13.0Enrico Tassi
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ta...Pierre-Marie Pédrot
2020-12-14Adding change log for #13568.Hugo Herbelin
2020-12-13Add changelog for #13509.Hugo Herbelin
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral n...coqbot-app[bot]
2020-12-11Merge PR #13611: Clarify changelog categories.Clément Pit-Claudel
2020-12-11Clarify changelog categories.Théo Zimmermann
2020-12-09Redefines exp_ineq1 to hold for all non-zero numbers.Avi Shinnar
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
2020-12-06[doc] update changes after 13501Enrico Tassi
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-04Merge PR #13442: Add an abstraction function in the LtacX FFI.coqbot-app[bot]
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
2020-12-03Ascii: add leb and ltbYishuai Li
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Changes for Coq 8.13Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-12 03:23:45 +0000