| Commit message (Expand) | Author | Age |
* | 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 |
* | Fixing too restrictive detection of resolution of evars in "apply in" | Hugo Herbelin | 2014-08-16 |
* | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau | 2014-08-14 |
* | Fix test-suite files according to new parsing rule for application of primitive | Matthieu Sozeau | 2014-08-13 |
* | Upgrading output tests. | Hugo Herbelin | 2014-08-12 |
* | Bug #3469: fixing unterminated comment. | Hugo Herbelin | 2014-08-12 |
* | In bug #2406, renouncing to test failure of parsing error. | Hugo Herbelin | 2014-08-12 |
* | Fix unification which was failing when unifying a primitive projection against | Matthieu Sozeau | 2014-08-09 |
* | Fix evarconv not applying eta when it used to. Fixes bug#3319. | Matthieu Sozeau | 2014-08-08 |
* | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | 2014-08-05 |
* | Fixing #3483 (graceful failing with notations to non-constructors in "match"). | Hugo Herbelin | 2014-08-03 |
* | Finish fixes on notations and primitive projections, add test-suite files for... | Matthieu Sozeau | 2014-07-31 |
* | Add test-suite file for bug #3439. | Matthieu Sozeau | 2014-07-30 |
* | Add test-suite file for bug 3454. | Matthieu Sozeau | 2014-07-29 |
* | Add test-suite file for bug #3453 | Matthieu Sozeau | 2014-07-29 |
* | fixup fakeide test-suite | Pierre Boutillier | 2014-07-24 |
* | Add test-suite file for guard condition on cofixpoints. | Maxime Dénès | 2014-07-22 |
* | Fixing output test-suite. | Pierre-Marie Pédrot | 2014-07-21 |
* | Adding a test-suite for bug #3422. | Pierre-Marie Pédrot | 2014-07-21 |
* | Adding a test-suite for bug #3416. | Pierre-Marie Pédrot | 2014-07-16 |
* | Fix Funind test-suite file after patch by Pierre. | Matthieu Sozeau | 2014-07-11 |
* | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey | 2014-07-09 |
* | Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl... | Matthieu Sozeau | 2014-07-03 |
* | Indeed simpl never is really honored now. | Matthieu Sozeau | 2014-07-02 |
* | Tests for bugs #2834 and #2994. | Hugo Herbelin | 2014-06-30 |
* | Completing test for bug report #2830 | Hugo Herbelin | 2014-06-30 |
* | Synchronized names from the "as" clause with the skeleton of the | Hugo Herbelin | 2014-06-30 |
* | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin | 2014-06-28 |
* | Invalid bug report. | Matthieu Sozeau | 2014-06-26 |
* | Fix bug # 3325 using canonical structure declarations where needed. | Matthieu Sozeau | 2014-06-26 |
* | Add an option to disable typeclass resolution during conversion, which | Matthieu Sozeau | 2014-06-26 |