aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/opened
Commit message (Expand)AuthorAge
* Fixing #4256 and #4484 (changes in evar-evar resolution made that newGravatar Hugo Herbelin2016-01-12
* Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
* Now closed.Gravatar Matthieu Sozeau2015-11-11
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Univs: fixed 3685 by side-effect :)Gravatar Matthieu Sozeau2015-10-02
* Univs: fix test-suite file for HoTT/coq bug #120Gravatar Matthieu Sozeau2015-10-02
* Tests for bugs #3509 and #3510.Gravatar Pierre-Marie Pédrot2015-07-28
* Remove old test file for #3819 (now fixed).Gravatar Maxime Dénès2015-07-16
* Removing test for opened bugs that were already present in the closed test-su...Gravatar Pierre-Marie Pédrot2015-05-18
* Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Gravatar Pierre-Marie Pédrot2015-05-18
* 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
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Updating test-suite (see previous commit).Gravatar Hugo Herbelin2015-03-24
* 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
* 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
* 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
* 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
* Moving test for bug #3071.Gravatar Pierre-Marie Pédrot2015-02-21
* Test for bug #3490.Gravatar Pierre-Marie Pédrot2015-02-15
* Adding test for bug #3786.Gravatar Pierre-Marie Pédrot2015-02-11
* 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
* Test #3655 was failing due to an anomaly. Now it rather has to failGravatar Hugo Herbelin2014-11-08
* Test fixed by PMP's commits from Oct 21.Gravatar Hugo Herbelin2014-11-08
* test suite: some reproduction cases for recently-reported bugs.Gravatar Xavier Clerc2014-11-04
* New bugs revealed fixed: #3408 by (probably) Maxime's commitsGravatar Hugo Herbelin2014-11-03
* More precise test for #3459.Gravatar Hugo Herbelin2014-10-21
* Bug fixed by Hugo.Gravatar Matthieu Sozeau2014-10-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 17:27:42 +0000