| Age | Commit message (Expand) | Author |
|---|
| 2015-10-09 | Refine fix for handling of the universe contexts of hints, depending on | Matthieu Sozeau |
| 2015-10-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-08 | Univs: fix bug #4161. | Matthieu Sozeau |
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi |
| 2015-10-07 | 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-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-06 | Fix bug #4354: interpret hints in the right env and sigma. | Matthieu Sozeau |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-02 | 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-09-26 | Test for bug #4347. | Pierre-Marie Pédrot |
| 2015-09-25 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-09-25 | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot |
| 2015-09-20 | Test file for #3948 - Anomaly: unknown constant in Print Assumptions. | Maxime Dénès |
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès |
| 2015-09-16 | In pat/constr introduction patterns, fixing in a better way clearing problems | Hugo Herbelin |
| 2015-09-15 | Test for bug #4269. | Pierre-Marie Pédrot |
| 2015-09-15 | STM: Reset takes Ltac <ident> into account (Close #4316) | Enrico Tassi |
| 2015-09-09 | Merge remote-tracking branch 'origin/v8.5' into trunk | Hugo Herbelin |
| 2015-09-08 | Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits | Hugo Herbelin |
| 2015-09-08 | Ensuring that patterns of the form pat/constr move the hypotheses replacing | Hugo Herbelin |
| 2015-09-08 | Documenting the new behaviour of the Shrink Obligations flag. | Pierre-Marie Pédrot |
| 2015-09-06 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-09-03 | Update test-suite after 518049fe7. | Maxime Dénès |
| 2015-08-22 | Documenting the Shrink Abstract option. | Pierre-Marie Pédrot |
| 2015-08-22 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-08-21 | Fixing #4318 (anomaly when applying args to a recursive notation in patterns). | Hugo Herbelin |
| 2015-08-14 | Move type_scope into user space, fix some output logs | Jason Gross |
| 2015-08-14 | Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 | Jason Gross |
| 2015-08-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-08-03 | Test file for #4254: Mutual inductives with parameters on Type raises anomaly. | Maxime Dénès |
