aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
Commit message (Expand)AuthorAge
...
* | | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...Gravatar Maxime Dénès2017-09-25
|\ \ \
* \ \ \ Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...Gravatar Maxime Dénès2017-09-25
|\ \ \ \
| | * | | Fixing #5755 (discharging of inductive types not correct with let-ins).Gravatar Hugo Herbelin2017-09-23
| |/ / / |/| | |
| * | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Gravatar Hugo Herbelin2017-09-23
* | | | A possible fix to BZ#5750 (ability to print context of ltac subterm match).Gravatar Hugo Herbelin2017-09-21
|/ / /
| | * ssr: fix canonical strucut key comparison with primproj onGravatar Enrico Tassi2017-09-20
| * | Fixing bug #5741 (anomaly in info_trivial).Gravatar Hugo Herbelin2017-09-19
|/ /
* | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Maxime Dénès2017-09-19
|\ \ | |/ |/|
* | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...Gravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Gravatar Maxime Dénès2017-09-15
|\ \ \
* \ \ \ Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match anon...Gravatar Maxime Dénès2017-09-15
|\ \ \ \
| | | | * Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Guillaume Melquiond2017-09-14
| |_|_|/ |/| | |
* | | | Addressing BZ#5713 (classical_left/classical_right artificially restricted).Gravatar Hugo Herbelin2017-09-03
* | | | Merge PR #996: Fix BZ#5697: Congruence does not work with primitive projectionsGravatar Maxime Dénès2017-08-31
|\ \ \ \
* \ \ \ \ Merge PR #995: Program: fix BZ#5683, missing lift when building case predicateGravatar Maxime Dénès2017-08-31
|\ \ \ \ \
* \ \ \ \ \ Merge PR #994: Fix BZ#5245 hnf on projections with simpl never flagGravatar Maxime Dénès2017-08-31
|\ \ \ \ \ \
| | | | | | * Fixing part of #5707 (allowing destruct to use non dependent case analysis).Gravatar Hugo Herbelin2017-08-30
| | | * | | | Properly handling parameters of primitive projections in cctac.Gravatar Pierre-Marie Pédrot2017-08-29
| | | * | | | Fix BZ#5697: Congruence does not work with primitive projections.Gravatar Pierre-Marie Pédrot2017-08-29
| |_|/ / / / |/| | | | |
* | | | | | Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #773: [flags] Remove XML output flag.Gravatar Maxime Dénès2017-08-29
|\ \ \ \ \ \ \ | |_|_|_|_|_|/ |/| | | | | |
| | * | | | | Dropping former fix to bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-08-29
| | * | | | | A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
| |/ / / / / |/| | | | |
| | * | | | primproj: fix bug 5245, hnf on proj with simpl never flag.Gravatar Matthieu Sozeau2017-08-25
| |/ / / / |/| | | |
| | * | | Program: fix BZ#5683, missing lift when building case predicateGravatar Matthieu Sozeau2017-08-24
| |/ / / |/| | |
| | | * Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
| |_|/ |/| |
* | | 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
| | | * | [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
| |_|/ / |/| | |
* | | | 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
| |/ / / |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-20 02:05:08 +0000