aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
2018-09-26Merge PR #8171: Bvector: add BVeq and some notationsHugo Herbelin
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-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
2018-07-16Update CHANGESJason Gross
2018-07-16bin,oct,hex conversions positive,Z,N,nat<->stringJason Gross
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-08Mention the removal of Emacs modes in CHANGES.Théo Zimmermann
2018-07-07Merge PR #7921: Archive the `gallina` toolMaxime Dénès
2018-07-03Document attributes.Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:44:40 +0000