aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Adding test for bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Another example about the consequence of a wrong computation of theGravatar Hugo Herbelin2015-03-25
* Updating test-suite (see previous commit).Gravatar Hugo Herbelin2015-03-24
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
* Fixing wrong rel_context in checking positivity condition.Gravatar Hugo Herbelin2015-03-24
* Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22
* Add some tests for tryifGravatar Jason Gross2015-03-13
* 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
* Do not display the status of monomorphic constants unless in universe-polymor...Gravatar Guillaume Melquiond2015-03-09
* Test for bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
* Test for #4035 (dependent destruction from Ltac).Gravatar Hugo Herbelin2015-03-07
* Fix testsuite with respect to the new formatting of Fail messages.Gravatar Guillaume Melquiond2015-03-05
* 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
* Add a test-suite file ensuring coinductives with primitive projectionsGravatar 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
* Fixing complexity tests for #4076.Gravatar Maxime Dénès2015-02-26
* Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."Gravatar Maxime Dénès2015-02-26
* Moving test for bug #3681 as closed.Gravatar Pierre-Marie Pédrot2015-02-26
* Another test for a variant of complexity problem #4076 (thanks to A. Mortberg).Gravatar Hugo Herbelin2015-02-25
* Univs: Fix Check calling the kernel to retype in the wrong environment.Gravatar Matthieu Sozeau2015-02-24
* Compensating 6fd763431 on postponing subtyping evar-evar problems.Gravatar Hugo Herbelin2015-02-23
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Test for #3953 (subst in evar instances).Gravatar Hugo Herbelin2015-02-23
* Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.Gravatar Hugo Herbelin2015-02-23
* Fixing occur-check which was too strong in unification.ml.Gravatar Hugo Herbelin2015-02-23
* Fixing test #2830.Gravatar Pierre-Marie Pédrot2015-02-23
* Fixing test for bug #3071.Gravatar Pierre-Marie Pédrot2015-02-23
* Moving test for bug #3071.Gravatar Pierre-Marie Pédrot2015-02-21
* Test for bug #4078.Gravatar Pierre-Marie Pédrot2015-02-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 02:22:39 +0000