| Age | Commit message (Expand) | Author |
|---|
| 2015-11-10 | Fixing #1225: we now skip the canonically built binding contexts of | Hugo Herbelin |
| 2015-11-10 | Merge origin/v8.5 into trunk | Hugo Herbelin |
| 2015-11-10 | Test for bug #4404. | Pierre-Marie Pédrot |
| 2015-11-07 | Merge remote-tracking branch 'origin/v8.5' into upstream-trunk | Hugo Herbelin |
| 2015-11-05 | Add test-suite file for #4273. | Matthieu Sozeau |
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-11-04 | Univs: missing checks in evarsolve with candidates and missing a | Matthieu Sozeau |
| 2015-11-04 | Fix bug in proofs/logic.ml type_of_global_reference_knowing_conclusion | Matthieu Sozeau |
| 2015-11-04 | Test file for #4397. | Maxime Dénès |
| 2015-11-02 | Fix bug #4151: discrepancy between exact and eexact/eassumption. | Matthieu Sozeau |
| 2015-11-02 | Refresh rigid universes as well, and in 8.4 compatibility mode, | Matthieu Sozeau |
| 2015-10-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-29 | Fixing another instance of bug #3267 in eauto, this time in the | Hugo Herbelin |
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-28 | Univs: fix bug #4375, accept universe binders on (co)-fixpoints | Matthieu Sozeau |
| 2015-10-27 | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names | Matthieu Sozeau |
| 2015-10-26 | Two test-suite files for bugs 3974 and 3975 | Pierre Letouzey |
| 2015-10-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-24 | Backtracking on interpreting toplevel calls to exact in scope determined | Hugo Herbelin |
| 2015-10-21 | Bug #3956 is fixed. | Matthieu Sozeau |
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-19 | Test for #4372 (anomaly in inversion in the presence of fake dependency). | Hugo Herbelin |
| 2015-10-17 | Test for bug #4325. | Pierre-Marie Pédrot |
| 2015-10-16 | Merge branch 'v8.5' into trunk | Maxime Dénès |
| 2015-10-15 | Test file for #4346: Set is no longer of type Type | Maxime Dénès |
| 2015-10-12 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-11 | Adding test for bug #4366. | Pierre-Marie Pédrot |
| 2015-10-10 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 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-07 | Fix bug #4069: f_equal regression. | Matthieu Sozeau |
| 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: 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 | Univs: fixed bug 2584, correct universe found for mutual inductive. | Matthieu Sozeau |
