aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2014-09-15Avoid backtracking in typeclass search if a solution for a closedMatthieu Sozeau
2014-09-15Rework typeclass resolution and control of backtracking.Matthieu Sozeau
2014-09-13Fixing injection bug #3616 on sigma-types.Hugo Herbelin
2014-09-12While we don't have a clean alternative to Clenvtac, add a primitiveMatthieu Sozeau
2014-09-12An old typo which was preventing example #3537 to work the same as itHugo Herbelin
2014-09-11Fix test-suite files, and move some opened to closed.Matthieu Sozeau
2014-09-11Other bugs with "inversion as" (collision between user-provided names and gen...Hugo Herbelin
2014-09-11Fix bug #3594: eta for constructors and functions at the same time whichMatthieu Sozeau
2014-09-11Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Matthieu Sozeau
2014-09-11Fix bug #3505.Matthieu Sozeau
2014-09-10Parsing and printing of primitive projections, fix buggy behavior whenMatthieu Sozeau
2014-09-10Fixing inversion after having fixed intros_replacingHugo Herbelin
2014-09-10Example for apply and evars.Hugo Herbelin
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
2014-09-08Fixing TestRefine test-suite file.Pierre-Marie Pédrot
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-08Parsing of Type@{max(i,j)}.Matthieu Sozeau
2014-09-07Test for "inversion as" naming bug.Hugo Herbelin
2014-09-07Regression test #3557Hugo Herbelin
2014-09-07Regression test for bug #2883.Hugo Herbelin
2014-09-06Fix bug #3584, elaborating pattern-matching on primitive records to theMatthieu Sozeau
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-05Fix primitive projections declarations for inductive records.Matthieu Sozeau
2014-09-04Status error for bug #3459.Pierre-Marie Pédrot
2014-09-04Test for bug #3459.Pierre-Marie Pédrot
2014-09-04Fix bug #3561, correct folding of env in context[] matching.Matthieu Sozeau
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
2014-09-04Add test-suite file for Case derivation on primitive records.Matthieu Sozeau
2014-09-04Add test suite files for closed bugs.Matthieu Sozeau
2014-09-04Fix bug #3563, making syntactic matching of primitive projectionsMatthieu Sozeau
2014-09-03Yes another remaining clearing bug with 'apply in'.Hugo Herbelin
2014-09-03Test-suite for bug #2818.Pierre-Marie Pédrot
2014-09-02Adding a test-suite for second-order matching order and indexes.Pierre-Marie Pédrot
2014-09-02Another fix than 19a7a5789c to avoid descend_in_conjunction to useHugo Herbelin
2014-09-02An apply test.Hugo Herbelin
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-29Not using a "cut" in descend_in_conjunctions induced more success. WeHugo Herbelin
2014-08-29Add test-suite file. Compute the name for the record binder in theMatthieu Sozeau
2014-08-28Fix bugs #3484 and #3546.Matthieu Sozeau
2014-08-28There are some occurs-check cases that can be handled by imitation (using pru...Matthieu Sozeau
2014-08-28Fixing an unnatural selection of subterms larger than expected in theHugo Herbelin
2014-08-28Adding test-suite for bug #3212.Pierre-Marie Pédrot
2014-08-26Add a regression test for 3427Jason Gross
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-08-25Fix computation of dangling constraints at the end of a proof (bug #3531).Matthieu Sozeau
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-25Grammar: "avoiding to" isn't proper, eitherJason Gross
2014-08-25Fixing a bug introduced in the extension of 'apply in' + simplifying code.Hugo Herbelin
2014-08-23Fix test-suite file.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 21:54:37 +0000