aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Test for "inversion as" naming bug.Gravatar Hugo Herbelin2014-09-07
* Regression test #3557Gravatar Hugo Herbelin2014-09-07
* Regression test for bug #2883.Gravatar Hugo Herbelin2014-09-07
* Fix bug #3584, elaborating pattern-matching on primitive records to theGravatar Matthieu Sozeau2014-09-06
* Fix checker to handle projections with eta and universe polymorphism correctly.Gravatar Matthieu Sozeau2014-09-06
* Fix primitive projections declarations for inductive records.Gravatar Matthieu Sozeau2014-09-05
* Status error for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Test for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Fix bug #3561, correct folding of env in context[] matching.Gravatar Matthieu Sozeau2014-09-04
* Fix bug #3559, ensuring a canonical order of universe level quantifications whenGravatar Matthieu Sozeau2014-09-04
* Add test-suite file for Case derivation on primitive records.Gravatar Matthieu Sozeau2014-09-04
* Add test suite files for closed bugs.Gravatar Matthieu Sozeau2014-09-04
* Fix bug #3563, making syntactic matching of primitive projectionsGravatar Matthieu Sozeau2014-09-04
* Yes another remaining clearing bug with 'apply in'.Gravatar Hugo Herbelin2014-09-03
* Test-suite for bug #2818.Gravatar Pierre-Marie Pédrot2014-09-03
* Adding a test-suite for second-order matching order and indexes.Gravatar Pierre-Marie Pédrot2014-09-02
* Another fix than 19a7a5789c to avoid descend_in_conjunction to useGravatar Hugo Herbelin2014-09-02
* An apply test.Gravatar Hugo Herbelin2014-09-02
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Not using a "cut" in descend_in_conjunctions induced more success. WeGravatar Hugo Herbelin2014-08-29
* Add test-suite file. Compute the name for the record binder in theGravatar Matthieu Sozeau2014-08-29
* Fix bugs #3484 and #3546.Gravatar Matthieu Sozeau2014-08-28
* There are some occurs-check cases that can be handled by imitation (using pru...Gravatar Matthieu Sozeau2014-08-28
* Fixing an unnatural selection of subterms larger than expected in theGravatar Hugo Herbelin2014-08-28
* Adding test-suite for bug #3212.Gravatar Pierre-Marie Pédrot2014-08-28
* Add a regression test for 3427Gravatar Jason Gross2014-08-26
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Fix computation of dangling constraints at the end of a proof (bug #3531).Gravatar Matthieu Sozeau2014-08-25
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Grammar: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
* Fixing a bug introduced in the extension of 'apply in' + simplifying code.Gravatar Hugo Herbelin2014-08-25
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-23
* Fixing unification of subterms identified by patterns.Gravatar Hugo Herbelin2014-08-18
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-18
* Fix test-suite files.Gravatar Matthieu Sozeau2014-08-18
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-18
* Fixing too restrictive detection of resolution of evars in "apply in"Gravatar Hugo Herbelin2014-08-16
* Restrict eta-conversion to inductive records, fixing bug #3310.Gravatar Matthieu Sozeau2014-08-14
* Fix test-suite files according to new parsing rule for application of primitiveGravatar Matthieu Sozeau2014-08-13
* Upgrading output tests.Gravatar Hugo Herbelin2014-08-12
* Bug #3469: fixing unterminated comment.Gravatar Hugo Herbelin2014-08-12
* In bug #2406, renouncing to test failure of parsing error.Gravatar Hugo Herbelin2014-08-12
* Fix unification which was failing when unifying a primitive projection againstGravatar Matthieu Sozeau2014-08-09
* Fix evarconv not applying eta when it used to. Fixes bug#3319.Gravatar Matthieu Sozeau2014-08-08
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Fixing #3483 (graceful failing with notations to non-constructors in "match").Gravatar Hugo Herbelin2014-08-03
* Finish fixes on notations and primitive projections, add test-suite files for...Gravatar Matthieu Sozeau2014-07-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 04:46:17 +0000