aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened
Commit message (Expand)AuthorAge
...
| * Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Gravatar Pierre-Marie Pédrot2015-05-18
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\|
* | #3953 now closed.Gravatar Hugo Herbelin2015-05-14
| * Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Gravatar Hugo Herbelin2015-05-09
| * Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forGravatar Hugo Herbelin2015-05-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* | Merge branch 'v8.5' into trunkGravatar Enrico Tassi2015-03-30
|\|
| * Updating test-suite (see previous commit).Gravatar Hugo Herbelin2015-03-24
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-11
|\|
| * admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| * Test for bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-04
|\|
| * Fix test-suite file, this is open.Gravatar Matthieu Sozeau2015-03-03
| * Add missing test-suite files and update gitignore.Gravatar Matthieu Sozeau2015-03-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-28
|\|
| * Fix test for #3848, still open.Gravatar Maxime Dénès2015-02-27
| * Moving test for #3467 to closed after PMP's fix.Gravatar Maxime Dénès2015-02-27
| * Fix test-suite files for bugs #2456 and #3593, still open.Gravatar Maxime Dénès2015-02-27
| * Moving tests for #2456 and #3593 to "opened" until they're fixed.Gravatar Maxime Dénès2015-02-27
| * Moving test of #3848 to "opened".Gravatar Maxime Dénès2015-02-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-26
|\|
| * Test for bug #3298.Gravatar Pierre-Marie Pédrot2015-02-26
| * Moving test for bug #3681 as closed.Gravatar Pierre-Marie Pédrot2015-02-26
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-23
|\|
| * Moving test for bug #3071.Gravatar Pierre-Marie Pédrot2015-02-21
* | Removed tests for #3900 and #3944 as open bugs.Gravatar Hugo Herbelin2015-02-21
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-15
|\|
| * Test for bug #3490.Gravatar Pierre-Marie Pédrot2015-02-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-13
|\|
| * Adding test for bug #3786.Gravatar Pierre-Marie Pédrot2015-02-11
* | Several reproduction cases for the test suite.Gravatar Xavier Clerc2015-01-28
* | Several reproduction cases for the test suite.Gravatar Xavier Clerc2015-01-28
* | Revert "Update test for #3363 now that Require is forbidden inside modules."Gravatar Maxime Dénès2015-01-18
| * Revert "Update test for #3363 now that Require is forbidden inside modules."Gravatar Maxime Dénès2015-01-17
|/
* Update test for #3363 now that Require is forbidden inside modules.Gravatar Maxime Dénès2015-01-12
* Fixing wrong notation level in #3295.Gravatar Hugo Herbelin2014-12-19
* #3828 is solved.Gravatar Hugo Herbelin2014-12-16
* Moving #2447 (congruence) to fixed.Gravatar Hugo Herbelin2014-12-16
* New reproduction cases for the test suite.Gravatar Xavier Clerc2014-12-11
* Commits on evar-evar unification fixed HoTT_coq_106 and improved theGravatar Hugo Herbelin2014-12-05
* Adding test for bug #3417.Gravatar Pierre-Marie Pédrot2014-11-30
* Test for bug #3487.Gravatar Pierre-Marie Pédrot2014-11-30
* Test of bug #3682.Gravatar Pierre-Marie Pédrot2014-11-30
* Bug #3804 is actually closed (thanks to Jason Gross for the notification).Gravatar Xavier Clerc2014-11-25
* Tweak some test cases.Gravatar Xavier Clerc2014-11-25
* Adding test for bug #3248.Gravatar Pierre-Marie Pédrot2014-11-24
* Cleaning up closed bugs in test-suite.Gravatar Pierre-Marie Pédrot2014-11-21
* Add missing "Fail" to test case for bug #2814.Gravatar Xavier Clerc2014-11-14
* Reproduction cases for the test suite.Gravatar Xavier Clerc2014-11-14