aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Expand)Author
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
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-07-01Document option Uniform Inductive ParametersJasper Hugunin
2018-06-28CHANGES for 8.8.1.Théo Zimmermann
2018-06-28Merge PR #7866: Implementation of mutual records in the higher strataMaxime Dénès
2018-06-27Fix #7723: vm_compute segfaults with universe polymorphismMaxime Dénès
2018-06-25Archive the `gallina` toolVincent Laporte
2018-06-24Added mention of mutual records to CHANGES.Pierre-Marie Pédrot
2018-06-22[ssr] implement {}/v as a short hand for {v}/v when v is an idEnrico Tassi
2018-06-22[ssr] simplify delayed clearsEnrico Tassi
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
2018-06-05Make direct invocations of `simple apply` obey `Opaque` directive.Maxime Dénès
2018-06-04Merge PR #7229: Deprecate implicit tactic solving.Hugo Herbelin
2018-06-04Merge PR #7486: Update old parts of CHANGES to use current bug numbers.Hugo Herbelin
2018-06-04Documenting the deprecation.Pierre-Marie Pédrot
2018-05-28Add CHANGES entryMaxime Dénès
2018-05-24[tactics] Remove anonymous fix/cofix form.Emilio Jesus Gallego Arias
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-17Document nested proofs and associated option.Théo Zimmermann
2018-05-11Update old parts of CHANGES to use current bug numbers.Théo Zimmermann
2018-05-11Notations: advertize that distinct "only parsing"/"only printing" rules work.Hugo Herbelin
2018-05-02Make "intro"/"intros" progress on existential variables.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:36:25 +0000