aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
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
2020-12-01Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0coqbot-app[bot]
2020-11-30Adding a changelog for Ltac1.lambda.Pierre-Marie Pédrot
2020-11-30Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumu...coqbot-app[bot]
2020-11-29Backport ssrbool lemmas from MathComp 1.12.0Kazuhiko Sakaguchi
2020-11-28Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."coqbot-app[bot]
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-app[bot]
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ...Matthieu Sozeau
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
2020-11-27Merge PR #13473: Testing {in _, _} and {pred _} from ssrboolcoqbot-app[bot]
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
2020-11-26[declare] Allow custom typing flags when declaring constants.Emilio Jesus Gallego Arias
2020-11-25Testing {in _, _} and {pred _} from ssrboolCyril Cohen
2020-11-25Changelog for #13415Gaëtan Gilbert
2020-11-25Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bugcoqbot-app[bot]
2020-11-25Merge PR #13405: Alternative implementation of the Micromega persistent cacheVincent Laporte
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-24Add a changelog.Pierre-Marie Pédrot
2020-11-24Fixing [dup] and [swap]Cyril Cohen
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notat...coqbot-app[bot]
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make s...coqbot-app[bot]
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the sam...Pierre-Marie Pédrot
2020-11-20Merge PR #13265: Add support for general non-necessarily-recursive binders in...coqbot-app[bot]
2020-11-20Merge PR #13352: Configure default value of -native-compilercoqbot-app[bot]
2020-11-20Add changelog for #13265.Hugo Herbelin
2020-11-20Add changelogPierre Roux
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...coqbot-app[bot]
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Adding change log.Hugo Herbelin
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
2020-11-20Update doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars...Hugo Herbelin
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a primiti...coqbot-app[bot]
2020-11-19Adding changelog for #13237.Hugo Herbelin
2020-11-19[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 20:43:16 +0000