aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog
AgeCommit message (Expand)Author
2020-08-27[zarith] ChangelogEmilio Jesus Gallego Arias
2020-08-27Merge PR #12862: [coqchk] Look inside inner modules as wellPierre-Marie Pédrot
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
2020-08-24Put cyclic numbers in sort Set instead of TypeVincent Semeria
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
2020-08-20Adding change log for PR #12816.Hugo Herbelin
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
2020-08-19Improve `make approve-output`Jason Gross
2020-08-19[coqchk] Look inside inner modules as wellJason Gross
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-08-18Fix subject reduction VS cumulative inductives and function etaGaëtan Gilbert
2020-08-13Merge PR #12799: [stdlib] [List] Additional statements about List.repeatAnton Trunov
2020-08-13Merge PR #12716: deprecate prod_curry and prod_uncurryAnton Trunov
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
2020-08-12Additional statements about List.repeatOlivier Laurent
2020-08-11add deprecation to changelogYishuai Li
2020-08-09Bring Int63 notations into line with stdlibJason Gross
2020-08-09Bring Float notations in line with stdlibJason Gross
2020-07-29coqdoc: Fix the “details” environmentThomas Letan
2020-07-28Merge PR #12754: Fixes #12752: applying symbol escaping in coqdoc indexLi-yao Xia
2020-07-24Adding change log for #12754.Hugo Herbelin
2020-07-23[changelog] Incorporate hanging changelog entry for 8.12+beta1Emilio Jesus Gallego Arias
2020-07-23[changelog] Fix hanging file extension.Emilio Jesus Gallego Arias
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-23Merge PR #12678: Tweak the warning for arbitrary term hints.Emilio Jesus Gallego Arias
2020-07-17Add a changelog.Pierre-Marie Pédrot
2020-07-17Merge PR #12683: Fixes #12682: printing bug with recursive notations for n-ar...Emilio Jesus Gallego Arias
2020-07-17Add changelog.Pierre-Marie Pédrot
2020-07-12Adding change log.Hugo Herbelin
2020-07-10Add changelog.Pierre-Marie Pédrot
2020-07-08Adding change log.Hugo Herbelin
2020-07-06Merge PR #11604: Primitive persistent arraysPierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-05Merge PR #12594: Fix ltac2 type parametersMichael Soegtrop
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-01Add a changelog.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 05:54:55 +0000