aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Expand)AuthorAge
* 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
* | | 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
| | | | * | Add opened bug 5019Gravatar 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
|/ / / / /
| | * | | Fix bug 5550: "typeclasses eauto with" does not work with section variables.Gravatar Théo Zimmermann2017-05-30
| * | | | Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Gravatar Pierre Letouzey2017-05-29
| |/ / /
| * | | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if prin...Gravatar Maxime Dénès2017-05-26
| |\ \ \
* | \ \ \ Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\ \ \ \ \
* | | | | | [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| * | | | | Using type classes in the interpretation of "specialize" and "contradiction".Gravatar Hugo Herbelin2017-05-22
|/ / / / /
| | * | | Fixing bug #5526,allow nonlinear variables in Notation patternsGravatar Paul Steckler2017-05-17
| * | | | fix swapping of ids in tuples, bug 5486Gravatar Paul Steckler2017-05-17
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\| | | |
| * | | | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Gravatar Hugo Herbelin2017-05-16
| |/ / /
| | * / Fix #5255: [Context (x : T := y)] should mean [Let x := y].Gravatar Pierre-Marie Pédrot2017-05-15
| |/ /
* | | Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 a...Gravatar Maxime Dénès2017-05-11
|\ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 07:25:53 +0000