| Age | Commit message (Expand) | Author |
|---|
| 2015-01-18 | Univs: Complete documentation in refman. | Matthieu Sozeau |
| 2015-01-18 | Partially revert "Forbid Require inside interactive modules and module types." | Maxime Dénès |
| 2015-01-18 | Revert "Adapting two files from test-suite to now forbidden Require's in modu... | Maxime Dénès |
| 2015-01-18 | Revert "Update test for #3363 now that Require is forbidden inside modules." | Maxime Dénès |
| 2015-01-18 | Revert "Fix files in test-suite having to do with Require inside modules." | Maxime Dénès |
| 2015-01-18 | Avoid compilation warning... might not be the best fix though. | Matthieu Sozeau |
| 2015-01-18 | Univs: Fix alias computation for VMs, computation of normal form of | Matthieu Sozeau |
| 2015-01-18 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès |
| 2015-01-18 | coq_makefile: install also .v and .glob | Enrico Tassi |
| 2015-01-18 | Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _" | Matthieu Sozeau |
| 2015-01-18 | vm_printers: fix compilation | Enrico Tassi |
| 2015-01-18 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-18 | Minor fixes to the refman credits to be continued. | Matthieu Sozeau |
| 2015-01-18 | Move explanations about primitive projections to the manual. | Matthieu Sozeau |
| 2015-01-18 | Add a (by default deactivated) option to force typeclass resolution to | Matthieu Sozeau |
| 2015-01-18 | Expand Credits for 8.5 and doc on universes | Matthieu Sozeau |
| 2015-01-18 | Remove typeclass opaque directive, some proofs in the stdlib rely on it being... | Matthieu Sozeau |
| 2015-01-18 | Optionally allow eta-conversion during unification for type classes. | Matthieu Sozeau |
| 2015-01-18 | Update header of CHANGES. | Maxime Dénès |
| 2015-01-18 | There was one more universe needed due to the use of now non-universe-polymor... | Matthieu Sozeau |
| 2015-01-17 | Back to 4 expected universes. | Matthieu Sozeau |
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau |
| 2015-01-17 | Univs: Complete documentation in refman. | Matthieu Sozeau |
| 2015-01-17 | Partially revert "Forbid Require inside interactive modules and module types." | Maxime Dénès |
| 2015-01-17 | Revert "Adapting two files from test-suite to now forbidden Require's in modu... | Maxime Dénès |
| 2015-01-17 | Revert "Update test for #3363 now that Require is forbidden inside modules." | Maxime Dénès |
| 2015-01-17 | Revert "Fix files in test-suite having to do with Require inside modules." | Maxime Dénès |
| 2015-01-17 | Avoid compilation warning... might not be the best fix though. | Matthieu Sozeau |
| 2015-01-17 | Univs: Fix alias computation for VMs, computation of normal form of | Matthieu Sozeau |
| 2015-01-17 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès |
| 2015-01-16 | coq_makefile: install also .v and .glob | Enrico Tassi |
| 2015-01-16 | Documenting the removal of coercions between sig, sigT, sig2, | Hugo Herbelin |
| 2015-01-16 | Documenting the removal of coercions between sig, sigT, sig2, | Hugo Herbelin |
| 2015-01-16 | Add two lemmas about firstn to the List standard library. | Sébastien Hinderer |
| 2015-01-16 | Lemmas related to the firstn function over lists. | Sébastien Hinderer |
| 2015-01-16 | ListSet: follow-up of Sebastien's last commit | Pierre Letouzey |
| 2015-01-16 | Work in progress on listset. | Sébastien Hinderer |
| 2015-01-16 | Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _" | Matthieu Sozeau |
| 2015-01-15 | Added stuff about -I -Q -R in COMPATIBILTY. | Pierre Courtieu |
| 2015-01-15 | vm_printers: fix compilation | Enrico Tassi |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-15 | Minor fixes to the refman credits to be continued. | Matthieu Sozeau |
| 2015-01-15 | Move explanations about primitive projections to the manual. | Matthieu Sozeau |
| 2015-01-15 | Add a (by default deactivated) option to force typeclass resolution to | Matthieu Sozeau |
| 2015-01-15 | Expand Credits for 8.5 and doc on universes | Matthieu Sozeau |
| 2015-01-15 | Remove typeclass opaque directive, some proofs in the stdlib rely on it being... | Matthieu Sozeau |
| 2015-01-15 | Optionally allow eta-conversion during unification for type classes. | Matthieu Sozeau |
| 2015-01-15 | Update header of CHANGES. | Maxime Dénès |
| 2015-01-15 | Revert "Bump version and magic numbers in configure." | Maxime Dénès |
| 2015-01-15 | Merge branch 'v8.5' into trunk | Maxime Dénès |
