| Commit message (Expand) | Author | Age |
* | Fix test suite after Matthieu's ed7af646f2e486b. | Maxime Dénès | 2015-10-28 |
* | test cases. | Gregory Malecha | 2015-10-28 |
* | Univs: fix bug #4375, accept universe binders on (co)-fixpoints | Matthieu Sozeau | 2015-10-28 |
* | Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins" | Hugo Herbelin | 2015-10-28 |
* | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names | Matthieu Sozeau | 2015-10-27 |
* | Two test-suite files for bugs 3974 and 3975 | Pierre Letouzey | 2015-10-26 |
* | Backtracking on interpreting toplevel calls to exact in scope determined | Hugo Herbelin | 2015-10-24 |
* | Fixing a bug in reporting ill-formed inductive. | Hugo Herbelin | 2015-10-22 |
* | Bug #3956 is fixed. | Matthieu Sozeau | 2015-10-21 |
* | Test for #4372 (anomaly in inversion in the presence of fake dependency). | Hugo Herbelin | 2015-10-19 |
* | Fixing #4198 (continued): not matching within the inner lambdas/let-ins | Hugo Herbelin | 2015-10-18 |
* | Test for bug #4325. | Pierre-Marie Pédrot | 2015-10-17 |
* | Test file for #4346: Set is no longer of type Type | Maxime Dénès | 2015-10-15 |
* | Fix some typos. | Guillaume Melquiond | 2015-10-13 |
* | Adding test for bug #4366. | Pierre-Marie Pédrot | 2015-10-11 |
* | Fixing test-suite | Hugo Herbelin | 2015-10-11 |
* | Fixing untimely unexpected warning "Collision between bound variables" (#4317). | Hugo Herbelin | 2015-10-11 |
* | Refining 0c320e79ba30 in fixing interpretation of constr under binders | Hugo Herbelin | 2015-10-11 |
* | Refine fix for handling of the universe contexts of hints, depending on | Matthieu Sozeau | 2015-10-09 |
* | Univs: fix bug #4161. | Matthieu Sozeau | 2015-10-08 |
* | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi | 2015-10-08 |
* | Fix bug #4069: f_equal regression. | Matthieu Sozeau | 2015-10-07 |
* | Test for record syntax parsing. | Pierre-Marie Pédrot | 2015-10-07 |
* | Univs: add Strict Universe Declaration option (on by default) | Matthieu Sozeau | 2015-10-07 |
* | Fix bug #4354: interpret hints in the right env and sigma. | Matthieu Sozeau | 2015-10-06 |
* | Univs: fix test-suite file for #4287, now properly rejected. | Matthieu Sozeau | 2015-10-02 |
* | Univs: Remove test-suite file #3309 | Matthieu Sozeau | 2015-10-02 |
* | Univs: fix test-suite file (4301 is invalid, but a good regression test) | Matthieu Sozeau | 2015-10-02 |
* | Univs: correct handling of with in modules | Matthieu Sozeau | 2015-10-02 |
* | Univs: the stdlib now needs 5 universes | Matthieu Sozeau | 2015-10-02 |
* | Univs: fix bug #4251, handling of template polymorphic constants. | Matthieu Sozeau | 2015-10-02 |
* | Univs: fixed 3685 by side-effect :) | Matthieu Sozeau | 2015-10-02 |
* | Univs: minor fixes to test-suite files | Matthieu Sozeau | 2015-10-02 |
* | Univs: fix test-suite file for HoTT/coq bug #120 | Matthieu Sozeau | 2015-10-02 |
* | Univs: test-suite file for bug #2016 | Matthieu Sozeau | 2015-10-02 |
* | Univs: test-suite file for #4301, subtyping of poly parameters | Matthieu Sozeau | 2015-10-02 |
* | Fix test-suite file for bug #3777 | Matthieu Sozeau | 2015-10-02 |
* | Fix test-suite file: failing earlier as expected. | Matthieu Sozeau | 2015-10-02 |
* | Fix test-suite file | Matthieu Sozeau | 2015-10-02 |
* | Univs: fixed bug 2584, correct universe found for mutual inductive. | Matthieu Sozeau | 2015-10-02 |
* | Univs: fix Universe vernacular, fix bug #4287. | Matthieu Sozeau | 2015-10-02 |
* | Univs: fixed bug #4328. | Matthieu Sozeau | 2015-10-02 |
* | Forcing i > Set for global universes (incomplete) | Matthieu Sozeau | 2015-10-02 |
* | Test for bug #4347. | Pierre-Marie Pédrot | 2015-09-26 |
* | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | 2015-09-25 |
* | Test file for #3948 - Anomaly: unknown constant in Print Assumptions. | Maxime Dénès | 2015-09-20 |
* | In pat/constr introduction patterns, fixing in a better way clearing problems | Hugo Herbelin | 2015-09-16 |
* | Test for bug #4269. | Pierre-Marie Pédrot | 2015-09-15 |
* | STM: Reset takes Ltac <ident> into account (Close #4316) | Enrico Tassi | 2015-09-15 |
* | Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits | Hugo Herbelin | 2015-09-08 |