aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-13Merge PR #12420: [stdlib] Decidable instance for negationcoqbot-app[bot]
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, no...coqbot-app[bot]
2020-11-12Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -Icoqbot-app[bot]
2020-11-12Add changelog for #13345.Hugo Herbelin
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
2020-11-11Add changelog for #13351.Hugo Herbelin
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
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-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