aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2018-10-05Rename CHANGES to CHANGES.md.Guillaume Melquiond
2018-10-05Improve markdown in changes.Guillaume Melquiond
2018-10-02Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0Pierre-Marie Pédrot
2018-10-01Merge PR #7634: Extend combined scheme to Schemes in TypeMatthieu Sozeau
2018-09-27A word about PR #262 in CHANGES.Hugo Herbelin
2018-09-26Merge PR #8171: Bvector: add BVeq and some notationsHugo Herbelin
2018-09-26[ocaml] Update required OCaml version to 4.05.0Emilio Jesus Gallego Arias
2018-09-26Merge PR #7309: Made names of existential variables interpretable as Ltac var...Pierre-Marie Pédrot
2018-09-26Merge PR #8419: Remove romega in favor of liaThéo Zimmermann
2018-09-26Combined Scheme tests sort to use either "*" or "/\"Théo Winterhalter
2018-09-26Merge PR #8217: Fixes #8215: "critical" type inference bug in interpreting ev...Pierre-Marie Pédrot
2018-09-25Merge PR #8235: NArith: deprecate N2Bv_genHugo Herbelin
2018-09-25Remove romegaVincent Laporte
2018-09-24Fixes #8215 ("critical" bug of type inference in interpreting evars by names).Hugo Herbelin
2018-09-20CHANGES for 8.8.2.Théo Zimmermann
2018-09-20Mention PDF doc in CHANGES.Théo Zimmermann
2018-09-19Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)Matthieu Sozeau
2018-09-14Fixing yet a source of dependency on alphabetic order in unification.Hugo Herbelin
2018-09-13Add entry for universe polymorphism critical bugGaëtan Gilbert
2018-09-12Remove quote pluginMaxime Dénès
2018-09-11Made names of existential variables interpretable as Ltac variables.Hugo Herbelin
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-10CHANGES: mentioning new command "Declare Scope".Hugo Herbelin
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-09-07Bvector: add BVeq and some notationsYishuai Li
2018-09-07NArith: deprecate N2Bv_genYishuai Li
2018-09-06Bound proof-search in default program obligation tactic.Matthieu Sozeau
2018-08-31Make Numeral Notation follow Import, not RequireJason Gross
2018-08-31Update CHANGESJason Gross
2018-08-29Move CHANGES entry for #8167 to 8.8.2 sectionJason Gross
2018-08-29Merge PR #8167: Fix ordering of before/after in print-pretty-timed-*Enrico Tassi
2018-08-27Document focusing on named goals.Théo Zimmermann
2018-08-24Fix ordering of before/after in print-pretty-timed-*Jason Gross
2018-08-01Merge PR #8169: NArith: add sized N2BvHugo Herbelin
2018-07-30CHANGES: unify formatYishuai Li
2018-07-30CHANGES: note potential incompatibilities with ++Yishuai Li
2018-07-30Vector: expose ++ to userYishuai Li
2018-07-30Merge PR #8137: Fix 8132. Print the content of body, not its type.Hugo Herbelin
2018-07-29Fix issue 8132. Print the content of body as in Printer.pr_compacted_decl,Jim Fehrle
2018-07-29Documenting custom entries in the reference manual + CHANGES.Hugo Herbelin
2018-07-26NArith: add sized N2BvYishuai Li
2018-07-25Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2)Hugo Herbelin
2018-07-24Merge PR #6801: Highlight differences between successive proof steps (color, ...Emilio Jesus Gallego Arias
2018-07-24Merge PR #8083: Add test for repeated section with same nameThéo Zimmermann
2018-07-24Merge PR #6597: Binary, Octal, and Hex conversions between [positive], [Z], [...Hugo Herbelin
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-07-23Add test for repeated section with same nameJasper Hugunin
2018-07-19Remove declare_object for SsrHave NoTCResolution.Maxime Dénès
2018-07-17Remove fourier pluginMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:43:55 +0000