aboutsummaryrefslogtreecommitdiff
path: root/CHANGES.md
AgeCommit message (Expand)Author
2019-04-23[ssr] under: Add doc for {under, over} & Add entry in CHANGES.mdErik Martin-Dorel
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-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
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
2019-01-22Update CHANGES.mdEnrico
2019-01-22Apply suggestions from code reviewThéo Zimmermann
2019-01-21[ssr] better structure the ipats docEnrico Tassi
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
2019-01-18[ssr] compile "=> {} y" as "=> {y} y"Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:49:24 +0000