aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Expand)Author
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-08-16Merge PR #942: solving b1859Maxime Dénès
2017-08-16Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsMaxime Dénès
2017-08-15Adding a test for BZ#1859 as suggested by @tchajed.Théo Zimmermann
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-08-01Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Maxime Dénès
2017-08-01Merge PR #926: test-suite uses Extraction TestCompileMaxime Dénès
2017-08-01Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Maxime Dénès
2017-07-29closing bug 5315Julien Forest
2017-07-27Fixing bug #5671 (specialize unclean wrt Metas).Hugo Herbelin
2017-07-27test-suite: more use of the new command Extraction TestCompilePierre Letouzey
2017-07-26Enrich test file 4720.v with a compilation test of the extracted codePierre Letouzey
2017-07-26adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...Pierre Letouzey
2017-07-26Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...Maxime Dénès
2017-07-25Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...Pierre Letouzey
2017-07-20Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Pierre Letouzey
2017-07-13Removing the uses of abstraction-breaking code in Lemmas.Pierre-Marie Pédrot
2017-07-11Fix nonsensical universe abstraction in the kernel.Pierre-Marie Pédrot
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-30Merge PR#843: closing bug #5618 introduce by PR 828Maxime Dénès
2017-06-29closing bug #5618 introduce by PR 828Julien Forest
2017-06-28A fix for #5598 (no discharge of Existing Classes referring to local variables).Hugo Herbelin
2017-06-26Merge PR#828: closing bug #4250Maxime Dénès
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-23closing bug #4250Julien Forest
2017-06-19Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalMaxime Dénès
2017-06-19Merge PR#613: Cumulativity for inductive typesMaxime Dénès
2017-06-19Test case for bug 5578.Maxime Dénès
2017-06-18Addressing #5434 (ltac pattern-matching refusing to match anonymous variables).Hugo Herbelin
2017-06-16Increase the time limit on 4366.v to make gitlab work better.Gaëtan Gilbert
2017-06-16Disable debug printingAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-15Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsMaxime Dénès
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-14[typeclasses eauto] Fix bug #3943: non-termination in topologicalMatthieu Sozeau
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-06-09A fix to #5414 (ident bound by ltac names now known for "match").Hugo Herbelin
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-08Adding a test case as requested in bug 5205.Théo Zimmermann
2017-06-06Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Maxime Dénès
2017-06-05Univs: fix bug #5365, generation of u+k <= v constraintsMatthieu Sozeau
2017-06-02Merge PR#705: Fix bug #5019 (looping zify on dependent types)Maxime Dénès
2017-06-01Merge PR#631: Fix bug #5255Maxime Dénès
2017-06-01Fix bug #5019 (looping zify on dependent types)Jason Gross
2017-05-31Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 21:44:45 +0000