aboutsummaryrefslogtreecommitdiff
path: root/CHANGES.md
AgeCommit message (Expand)Author
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
2019-04-04Update CHANGES.mdPierre Roux
2019-04-03Merge PR #9078: Provide a faster bound name generation algorithm through a flagVincent Laporte
2019-04-03Merge PR #8638: Remove -compat 8.7Théo Zimmermann
2019-04-02Merge PR #9668: Consolidate credits and changelog information in a single place.Clément Pit-Claudel
2019-04-02Remove -compat 8.7Jason Gross
2019-04-02Document the Fast Name Printing option.Pierre-Marie Pédrot
2019-04-01Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and ...Vincent Laporte
2019-04-01Update CHANGESJason Gross
2019-04-01Several improvements and fixes of LiaFrédéric Besson
2019-04-01Merge PR #9872: Fix timing diff script to support non-utf8Emilio Jesus Gallego Arias
2019-03-31[pretty-timing scripts] Don't barf on non-utf-8Jason Gross
2019-03-31Move V8 CHANGES to Changes chapter.Théo Zimmermann
2019-03-31Move V7 CHANGES to History chapter.Théo Zimmermann
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
2019-03-27Deprecate `Refine Instance Mode` optionMaxime Dénès
2019-03-26Merge PR #9829: [Vernacular] Deprecate the “Show Script” commandEnrico Tassi
2019-03-25[Vernacular] Deprecate the “Show Script” commandVincent Laporte
2019-03-25Remove `Automatic Coercions Import` option.Maxime Dénès
2019-03-22Merge PR #8560: Unicode bindings for CoqIDE that works out of the boxPierre-Marie Pédrot
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ...Maxime Dénès
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
2019-03-19CoqIDE: Advertising gtk+3 upgrade in CHANGES.Hugo Herbelin
2019-03-18Update doc and changesKazuhiko Sakaguchi
2019-03-18fix documentation issues, and add entry to change logcharguer
2019-03-15Merge PR #8817: SProp: the definitionally proof irrelevant universePierre-Marie Pédrot
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14BinInt: 3 lemmas about testbit, mod _ 2^, onesAndres Erbsen
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-02-28Fix #7632: Change syntax of autoapply according to the documentation.Théo Zimmermann
2019-02-22update CHANGESEnrico Tassi
2019-02-22Apply implicit binders to Hypothesis inside sections.Jasper Hugunin
2019-02-22Merge PR #9314: Enrich implicits for instancesGaëtan Gilbert
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-11Fix #9508: Unexpected interaction between implicit arguments and primitive pr...Pierre-Marie Pédrot
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
2019-02-05Add an option not to register Ltac backtraces.Pierre-Marie Pédrot
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Enrich implicits for instancesJasper Hugunin
2019-02-04Primitive integersMaxime Dénès
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
2019-01-25Added a line about notation bug fixes.Hugo Herbelin
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_div...Jason Gross
2019-01-24Update CHANGESJason Gross
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 17:30:36 +0000