aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2020-11-09Merge PR #13217: Addresses #13216: use of type classes in the return clause o...Pierre-Marie Pédrot
2020-11-06Merge PR #13139: Clean the constr-as-hint APIcoqbot-app[bot]
2020-11-06Update doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rstCyril Cohen
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
2020-11-06Intro pattern extensions for dup, swap and applyCyril Cohen
2020-11-05Added change log for #12099.Hugo Herbelin
2020-11-05Adding change log for #13217.Hugo Herbelin
2020-11-05Changelog for 8.12.1.Théo Zimmermann
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-05Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ...coqbot-app[bot]
2020-11-04[stdlib] Decidable instance for negationYishuai Li
2020-11-05Add changelogPierre Roux
2020-11-04Document the syntax addition.Pierre-Marie Pédrot
2020-11-04Adding change log for #13255.Hugo Herbelin
2020-11-04Adding change log for #13301.Hugo Herbelin
2020-11-04Document the changes.Pierre-Marie Pédrot
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding not...coqbot-app[bot]
2020-11-02Merge PR #13183: attribute #[using] for Definition and Fixpointcoqbot-app[bot]
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ...Pierre-Marie Pédrot
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-11-02add changelogEnrico Tassi
2020-10-31Adding overlay for PR #13290.Hugo Herbelin
2020-10-30Add change log for #13145.Hugo Herbelin
2020-10-28Adding changelog for #13247.Hugo Herbelin
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-19Adding change log for #13092.Hugo Herbelin
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