aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2017-09-19Fixing bug #5741 (anomaly in info_trivial).Hugo Herbelin
2017-09-19Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Maxime Dénès
2017-09-15Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...Maxime Dénès
2017-09-15Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Maxime Dénès
2017-09-15Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...Maxime Dénès
2017-09-14Avoid extra failure in the "constructor" tactic (bug #5666).Guillaume Melquiond
2017-09-03Addressing BZ#5713 (classical_left/classical_right artificially restricted).Hugo Herbelin
2017-08-31Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projectionsMaxime Dénès
2017-08-31Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateMaxime Dénès
2017-08-31Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagMaxime Dénès
2017-08-30Fixing part of #5707 (allowing destruct to use non dependent case analysis).Hugo Herbelin
2017-08-29Properly handling parameters of primitive projections in cctac.Pierre-Marie Pédrot
2017-08-29Fix BZ#5697: Congruence does not work with primitive projections.Pierre-Marie Pédrot
2017-08-29Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...Maxime Dénès
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29Dropping former fix to bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-25primproj: fix bug 5245, hnf on proj with simpl never flag.Matthieu Sozeau
2017-08-24Program: fix BZ#5683, missing lift when building case predicateMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 03:14:43 +0000