aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...coqbot-app[bot]
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-20[zify] Add support for Int63.intFrédéric Besson
2020-10-16Add change log for #13166.Hugo Herbelin
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
2020-10-12Merge PR #12449: Minimize Prop <= i to i := Setcoqbot-app[bot]
2020-10-10Adding change log for #12950.Hugo Herbelin
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
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-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ...coqbot-app[bot]
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lon...coqbot-app[bot]
2020-09-23Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)coqbot-app[bot]
2020-09-23Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of quotatio...Pierre-Marie Pédrot
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
2020-09-22Merge PR #13067: Setting default value for Display Parentheses off in CoqIDEcoqbot-app[bot]
2020-09-22Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested applica...coqbot-app[bot]
2020-09-22Adding change log for #12794 and #13067.Hugo Herbelin
2020-09-22Adding change log for #13028.Hugo Herbelin
2020-09-21Make print-pretty-timed robust against non-output-sync logsJason Gross
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
2020-09-15Adding change log for #13026.Hugo Herbelin
2020-09-15Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"Pierre-Marie Pédrot
2020-09-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
2020-09-14[ci] [docker] Up testing to OCaml 4.11.1Emilio Jesus Gallego Arias
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-09-11Minimal changes to make the refman compatible with Sphinx 3.Théo Zimmermann
2020-09-10Merge PR #12998: changelog entry for 12857coqbot-app[bot]
2020-09-10Update doc/changelog/06-ssreflect/12857-changelog-for-12857.rstEnrico Tassi
2020-09-09Merge PR #12094: Extend app_inj_tail and other list lemmasHugo Herbelin
2020-09-09changelog entry for 12857Enrico Tassi
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...Pierre-Marie Pédrot
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-09-07Add changelog entryEdward Wang
2020-09-02Adding change log for #12960.Hugo Herbelin
2020-09-02Adding change log for #12946.Hugo Herbelin
2020-08-27[zarith] ChangelogEmilio Jesus Gallego Arias
2020-08-27Merge PR #12862: [coqchk] Look inside inner modules as wellPierre-Marie Pédrot
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
2020-08-20Adding change log for PR #12816.Hugo Herbelin
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
2020-08-19Improve `make approve-output`Jason Gross