aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Expand)AuthorAge
* Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Gravatar Pierre-Marie Pédrot2015-05-18
* Removing option -no-native-compiler from test #3539 since this option is nowGravatar Hugo Herbelin2015-05-15
* Fixing bug #4216:Gravatar Pierre-Marie Pédrot2015-05-13
* Better fixing #4198 such that the term to match is looked for beforeGravatar Hugo Herbelin2015-05-13
* Test for bug #4234.Gravatar Pierre-Marie Pédrot2015-05-12
* Test for bug #4232.Gravatar Pierre-Marie Pédrot2015-05-11
* 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
* Fixing computation of implicit arguments by position in fixpoints (#4217).Gravatar Hugo Herbelin2015-05-01
* Giving to "subst" a more natural semantic (fixing #4214) by using allGravatar Hugo Herbelin2015-05-01
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Test for #4198 (appcontext in return clause of match).Gravatar Hugo Herbelin2015-04-22
* Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argumentGravatar Hugo Herbelin2015-04-21
* Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalGravatar Hugo Herbelin2015-04-17
* Test for bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* Test for bug #3199.Gravatar Pierre-Marie Pédrot2015-04-10
* Better test-suite files, removing reliance on admit.Gravatar Matthieu Sozeau2015-04-09
* Fix declarations of instances to perform restriction of universeGravatar Matthieu Sozeau2015-04-09
* Add test-suite file for bug #4120.Gravatar Matthieu Sozeau2015-04-09
* Test for bug #3815.Gravatar Pierre-Marie Pédrot2015-04-06
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-03-31
* Adding test for bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* Updating test-suite (see previous commit).Gravatar Hugo Herbelin2015-03-24
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
* Fix regression in HoTT_coq_014.vGravatar Enrico Tassi2015-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
* Test for #4035 (dependent destruction from Ltac).Gravatar Hugo Herbelin2015-03-07
* Fix test-suite file, this is open.Gravatar Matthieu Sozeau2015-03-03
* Fix bug #3732: firstorder was using detyping to build existentialGravatar Matthieu Sozeau2015-03-03
* Add missing test-suite files and update gitignore.Gravatar Matthieu Sozeau2015-03-03
* Fix test-suite file, this is currently a wontfix, but keep theGravatar Matthieu Sozeau2015-03-03
* Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeGravatar Matthieu Sozeau2015-03-03
* Fix bug #4101, noccur_evar's expand_projection can legitimately failGravatar Matthieu Sozeau2015-03-03
* Fix bug #4097.Gravatar Matthieu Sozeau2015-03-02
* Adding a test for bug #3612.Gravatar Pierre-Marie Pédrot2015-02-27
* Test for bug #3249.Gravatar Pierre-Marie Pédrot2015-02-27
* Fix test for #3467, I had moved it in a dumb way.Gravatar Maxime Dénès2015-02-27
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* Fixing first part of bug #3210 (inference of pattern-matching returnGravatar Hugo Herbelin2015-02-27
* 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
* Add test-suite file for #3649.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
* Made test for #3392 rely less on unification.Gravatar Maxime Dénès2015-02-27
* Moving test of #3848 to "opened".Gravatar Maxime Dénès2015-02-27
* Test for #2602, which seems now fixed.Gravatar Maxime Dénès2015-02-26
* Test for bug #3298.Gravatar Pierre-Marie Pédrot2015-02-26
* Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Gravatar Maxime Dénès2015-02-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 09:30:19 +0000