aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-03Merge PR #10390: UIP in SPropMaxime Dénès
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet pat...Gaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
2020-06-24[test-suite] Fix dependencies of modules/ filesJason Gross
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
2020-06-23Merge PR #12562: CoqIDE: accept to open files with invalid namesMichael Soegtrop
2020-06-22CoqIDE: accept to open files with invalid namesVincent Laporte
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
2020-06-11Merge PR #12423: Remove info tactic, deprecated in 8.5Pierre-Marie Pédrot
2020-06-10Update changelog for 8.12+beta1.Théo Zimmermann
2020-06-09Merge PR #12484: Fix #12483 Incorrect specification of PrimFloat.lebGuillaume Melquiond
2020-06-09CReal: changed epsilon for modulus of convergence from 1/n to 2^zMichael Soegtrop
2020-06-08Fix 12483Pierre Roux
2020-06-05Add remaining 8.12+beta1 changelog entries.Théo Zimmermann
2020-06-02Merge PR #11974: Require in Section: warning is now about fragility not depre...Emilio Jesus Gallego Arias
2020-06-01Merge PR #12396: Release notes 8.12Emilio Jesus Gallego Arias
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-29Change log for #12422.Hugo Herbelin
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
2020-05-27Adding changelog.Martin Bodin
2020-05-27Add more changelog entries which have been backported to v8.12.Théo Zimmermann
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-27Fix changelog for #11986.Théo Zimmermann
2020-05-26Merge PR #12410: dev/tools/make-changelog.sh now asks about fixed bugsGaëtan Gilbert
2020-05-26Merge PR #12388: Fix an uncaught python exception in timingGaëtan Gilbert
2020-05-25dev/tools/make-changelog.sh now asks about fixed bugsJason Gross
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
2020-05-25Add a changelog.Pierre-Marie Pédrot
2020-05-22[coqchk] Fix #5030Pierre Roux
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...Pierre-Marie Pédrot
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
2020-05-21Fix an uncaught python exception in timingJason Gross
2020-05-21Merge PR #12368: Print a newline at the end of timing tablesGaëtan Gilbert
2020-05-20Print a newline at the end of timing tablesJason Gross
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
2020-05-19[topfmt] Set formatter + flush fixEmilio Jesus Gallego Arias
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Bump minimal versions of refman dependencies.Théo Zimmermann
2020-05-17Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place ...Jason Gross
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-16Merge PR #12288: Prove that classical reals implement constructive reals.Michael Soegtrop
2020-05-16Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.Emilio Jesus Gallego Arias
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 09:07:23 +0000