aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Expand)AuthorAge
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-18
|\
* | Quick fix to unification regression #4955.Gravatar Hugo Herbelin2016-10-17
| * Fixing to #3209 (Not_found due to an occur-check cycle).Gravatar Hugo Herbelin2016-10-17
* | Merge PR #300 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\ \
* | | Fix bug #5145: Anomaly: index to an anonymous variable.Gravatar Pierre-Marie Pédrot2016-10-15
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \ \ | | |/ | |/|
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\ \ \
| | * | Merge remote-tracking branch 'git/bug5123' into v8.5Gravatar Matthieu Sozeau2016-10-12
| |/| |
| | * | Fix test-suite file 5123 to fail in case of regressionGravatar Matthieu Sozeau2016-10-11
| | * | Fix bug #5123: mark all shelved evars unresolvableGravatar Matthieu Sozeau2016-10-11
| * | | Fix for bug #4863, update the Proofview's env withGravatar Matthieu Sozeau2016-10-11
| |/ /
| * | Add test file for #4416.Gravatar Maxime Dénès2016-10-10
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-08
|\| |
* | | Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.Gravatar Pierre-Marie Pédrot2016-10-08
* | | Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Gravatar Pierre-Marie Pédrot2016-10-07
| * | evarconv.ml: Fix bug #4529, primproj unfoldingGravatar Matthieu Sozeau2016-10-06
| * | unification.ml: fix for bug #4763, unif regressionGravatar Matthieu Sozeau2016-10-06
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-05
|\| |
| * | Fixing #4970 (confusion between special "{" and non special "{{" in notations).Gravatar Hugo Herbelin2016-10-03
* | | Fix bug #4661: Cannot mask the absolute name.Gravatar Pierre-Marie Pédrot2016-10-01
* | | Fix bug #5045: [generalize] creates ill-typed terms in 8.6.Gravatar Pierre-Marie Pédrot2016-09-30
* | | Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk.Gravatar Pierre-Marie Pédrot2016-09-30
* | | Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \
* \ \ \ Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ | | |/ / | |/| |
| * | | Fix #4762.Gravatar Cyprien Mangin2016-09-30
| | | * Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
| |_|/ |/| |
* | | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
* | | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
* | | Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-09-29
|\ \ \
| * | | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-09-29
* | | | Merge branch 'bug4723' into v8.6Gravatar Matthieu Sozeau2016-09-29
|\ \ \ \
| | | | * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
| | | |/ | | |/|
* | / | Fix bug #5011: Anomaly on [Existing Class].Gravatar Pierre-Marie Pédrot2016-09-29
| |/ / |/| |
| * | Fix bug #4723 and FIXME in API for solve_by_tacGravatar Matthieu Sozeau2016-09-28
|/ /
* | Merge remote-tracking branch 'github/pr/232' into v8.6Gravatar Maxime Dénès2016-09-28
|\ \
* | | Add fixed test-suite file for bug #4527Gravatar Matthieu Sozeau2016-09-27
* | | Unbreak Ltac [ | .. | ] notation in -compat 8.5Gravatar Jason Gross2016-09-26
* | | Fix bug #4785 (use [ ] for vector nil)Gravatar Jason Gross2016-09-26
* | | Fix bug #5093: typeclasses eauto depth arg does not accept a var.Gravatar Pierre-Marie Pédrot2016-09-26
* | | Adding a test for bug #5096.Gravatar Pierre-Marie Pédrot2016-09-24
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-23
|\ \ \ | | |/ | |/|
| * | Fixing #5095 (non relevant too strict test in let-in abstraction).Gravatar Hugo Herbelin2016-09-22
* | | Continuing fix to #5078, taking also into account intropatterns.Gravatar Hugo Herbelin2016-09-15
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
|\| |
* | | Merge remote-tracking branch 'github-coq/pr/249' into v8.6Gravatar Matthieu Sozeau2016-09-12
|\ \ \
* | | | Add a test for 4836Gravatar Jason Gross2016-09-11
| | * | Test for #5077.Gravatar Hugo Herbelin2016-09-10
| * | | no-refold patchGravatar Paul Steckler2016-09-09
|/ / /
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-07
|\| |
| * | Test file for #5065 - Anomaly: Not a proof by inductionGravatar Maxime Dénès2016-09-05