| Commit message (Expand) | Author | Age |
|---|
| * | Fix test-suite files, and move some opened to closed. |  Matthieu Sozeau | 2014-09-11 |
| * | Other bugs with "inversion as" (collision between user-provided names and gen... |  Hugo Herbelin | 2014-09-11 |
| * | Fix bug #3594: eta for constructors and functions at the same time which | Matthieu Sozeau | 2014-09-11 |
| * | Fix bug #3596, wrong treatment of projections in compute_constelim_direct. | Matthieu Sozeau | 2014-09-11 |
| * | Fix bug #3505. | Matthieu Sozeau | 2014-09-11 |
| * | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau | 2014-09-10 |
| * | Fixing inversion after having fixed intros_replacing | Hugo Herbelin | 2014-09-10 |
| * | Example for apply and evars. | Hugo Herbelin | 2014-09-10 |
| * | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau | 2014-09-09 |
| * | Fixing TestRefine test-suite file. |  Pierre-Marie Pédrot | 2014-09-08 |
| * | Removing dead code relative to the XML plugin. | Pierre-Marie Pédrot | 2014-09-08 |
| * | Parsing of Type@{max(i,j)}. |  Matthieu Sozeau | 2014-09-08 |
| * | Test for "inversion as" naming bug. | Hugo Herbelin | 2014-09-07 |
| * | Regression test #3557 | Hugo Herbelin | 2014-09-07 |
| * | Regression test for bug #2883. | Hugo Herbelin | 2014-09-07 |
| * | Fix bug #3584, elaborating pattern-matching on primitive records to the | Matthieu Sozeau | 2014-09-06 |
| * | Fix checker to handle projections with eta and universe polymorphism correctly. | Matthieu Sozeau | 2014-09-06 |
| * | Fix primitive projections declarations for inductive records. | Matthieu Sozeau | 2014-09-05 |
| * | Status error for bug #3459. | Pierre-Marie Pédrot | 2014-09-04 |
| * | Test for bug #3459. | Pierre-Marie Pédrot | 2014-09-04 |
| * | Fix bug #3561, correct folding of env in context[] matching. | Matthieu Sozeau | 2014-09-04 |
| * | Fix bug #3559, ensuring a canonical order of universe level quantifications when | Matthieu Sozeau | 2014-09-04 |
| * | Add test-suite file for Case derivation on primitive records. | Matthieu Sozeau | 2014-09-04 |
| * | Add test suite files for closed bugs. | Matthieu Sozeau | 2014-09-04 |
| * | Fix bug #3563, making syntactic matching of primitive projections | Matthieu Sozeau | 2014-09-04 |
| * | Yes another remaining clearing bug with 'apply in'. | Hugo Herbelin | 2014-09-03 |
| * | Test-suite for bug #2818. | Pierre-Marie Pédrot | 2014-09-03 |
| * | Adding a test-suite for second-order matching order and indexes. | Pierre-Marie Pédrot | 2014-09-02 |
| * | Another fix than 19a7a5789c to avoid descend_in_conjunction to use | Hugo Herbelin | 2014-09-02 |
| * | An apply test. | Hugo Herbelin | 2014-09-02 |
| * | Simplify even further the declaration of primitive projections, | Matthieu Sozeau | 2014-08-30 |
| * | Not using a "cut" in descend_in_conjunctions induced more success. We | Hugo Herbelin | 2014-08-29 |
| * | Add test-suite file. Compute the name for the record binder in the | Matthieu Sozeau | 2014-08-29 |
| * | Fix bugs #3484 and #3546. | Matthieu Sozeau | 2014-08-28 |
| * | There are some occurs-check cases that can be handled by imitation (using pru... | Matthieu Sozeau | 2014-08-28 |
| * | Fixing an unnatural selection of subterms larger than expected in the | Hugo Herbelin | 2014-08-28 |
| * | Adding test-suite for bug #3212. | Pierre-Marie Pédrot | 2014-08-28 |
| * | Add a regression test for 3427 |  Jason Gross | 2014-08-26 |
| * | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau | 2014-08-25 |
| * | Fix computation of dangling constraints at the end of a proof (bug #3531). | Matthieu Sozeau | 2014-08-25 |
| * | "allows to", like "allowing to", is improper | Jason Gross | 2014-08-25 |
| * | instanciation is French, instantiation is English | Jason Gross | 2014-08-25 |
| * | Grammar: "avoiding to" isn't proper, either | Jason Gross | 2014-08-25 |
| * | Fixing a bug introduced in the extension of 'apply in' + simplifying code. | Hugo Herbelin | 2014-08-25 |
| * | Fix test-suite file. | Matthieu Sozeau | 2014-08-23 |
| * | Fixing unification of subterms identified by patterns. | Hugo Herbelin | 2014-08-18 |
| * | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin | 2014-08-18 |
| * | Fix test-suite file. | Matthieu Sozeau | 2014-08-18 |
| * | Fix test-suite files. | Matthieu Sozeau | 2014-08-18 |
| * | Fix test-suite file. | Matthieu Sozeau | 2014-08-18 |
Matthieu Sozeau
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau
Jason Gross