aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
Commit message (Expand)AuthorAge
* Fixing part of #5707 (allowing destruct to use non dependent case analysis).Gravatar Hugo Herbelin2017-08-30
* Merge PR #942: solving b1859Gravatar Maxime Dénès2017-08-16
|\
* \ Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsGravatar Maxime Dénès2017-08-16
|\ \
| | * Adding a test for BZ#1859 as suggested by @tchajed.Gravatar Théo Zimmermann2017-08-15
* | | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Gravatar Maxime Dénès2017-08-01
|\ \ \
* \ \ \ Merge PR #926: test-suite uses Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\ \ \ \
* \ \ \ \ Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Maxime Dénès2017-08-01
|\ \ \ \ \
* | | | | | closing bug 5315Gravatar Julien Forest2017-07-29
| |_|_|_|/ |/| | | |
| | | * | Fixing bug #5671 (specialize unclean wrt Metas).Gravatar Hugo Herbelin2017-07-27
| |_|/ / |/| | |
| | * | test-suite: more use of the new command Extraction TestCompileGravatar Pierre Letouzey2017-07-27
| | * | Enrich test file 4720.v with a compilation test of the extracted codeGravatar Pierre Letouzey2017-07-26
| |/ / |/| |
| * | adding a test-suite file 4709.v (thanks to the new command Extraction TestCom...Gravatar Pierre Letouzey2017-07-26
|/ /
* | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...Gravatar Maxime Dénès2017-07-26
|\ \
| * | Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...Gravatar Pierre Letouzey2017-07-25
* | | Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Gravatar Pierre Letouzey2017-07-20
|/ /
* | Removing the uses of abstraction-breaking code in Lemmas.Gravatar Pierre-Marie Pédrot2017-07-13
* | Fix nonsensical universe abstraction in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \
* \ \ Merge PR#843: closing bug #5618 introduce by PR 828Gravatar Maxime Dénès2017-06-30
|\ \ \
| * | | closing bug #5618 introduce by PR 828Gravatar Julien Forest2017-06-29
| | | * A fix for #5598 (no discharge of Existing Classes referring to local variables).Gravatar Hugo Herbelin2017-06-28
| |_|/ |/| |
* | | Merge PR#828: closing bug #4250Gravatar Maxime Dénès2017-06-26
|\| |
* | | Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \ \
| | * | closing bug #4250Gravatar Julien Forest2017-06-23
| |/ / |/| |
* | | Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Maxime Dénès2017-06-19
|\ \ \
* \ \ \ Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \ \ \
* | | | | Test case for bug 5578.Gravatar Maxime Dénès2017-06-19
* | | | | Increase the time limit on 4366.v to make gitlab work better.Gravatar Gaëtan Gilbert2017-06-16
| * | | | Disable debug printingGravatar Amin Timany2017-06-16
| * | | | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/ / / /
| | | * Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Maxime Dénès2017-06-15
| | | |\
* | | | \ Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\ \ \ \ \
| | | * | | plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
* | | | | | Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | |
* | | | | | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \ \
| | | | * | | [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Matthieu Sozeau2017-06-14
* | | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| |_|_|/ / / |/| | | | |
| | | * | | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |_|/ / / |/| | | |
| | * | | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ / / |/| | |
| * | | A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/ / /
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ \
| | * | Adding a test case as requested in bug 5205.Gravatar Théo Zimmermann2017-06-08
| |/ /
* | | Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Gravatar Maxime Dénès2017-06-06
|\ \ \
| | | * Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
| | * | Merge PR#705: Fix bug #5019 (looping zify on dependent types)Gravatar Maxime Dénès2017-06-02
| | |\ \
| | * \ \ Merge PR#631: Fix bug #5255Gravatar Maxime Dénès2017-06-01
| | |\ \ \
| | | | * | Fix bug #5019 (looping zify on dependent types)Gravatar Jason Gross2017-06-01
| | | |/ / | | |/| |
| | * | | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with secti...Gravatar Maxime Dénès2017-05-31
| | |\ \ \
| * | | | | Fixing #5233 (missing implicit arguments for recursive records).Gravatar Hugo Herbelin2017-05-31
* | | | | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
|/ / / / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 09:20:04 +0000