| Age | Commit message (Expand) | Author |
|---|
| 2015-01-21 | Add the possibility of defining opaque terms with program. | mlasson |
| 2015-01-21 | Reference Manual/Credits: expand the paragraph on the new proof engine to mat... | Arnaud Spiwack |
| 2015-01-21 | Reference Manual/Credits: native compute is a major contribution. | Arnaud Spiwack |
| 2015-01-21 | Reference manual/Credits: populate the "various smaller-scale improvements" p... | Arnaud Spiwack |
| 2015-01-21 | Reference Manual/Credits: remove a duplicate. | Arnaud Spiwack |
| 2015-01-21 | Reference manual: pass over the credit section for English. | Arnaud Spiwack |
| 2015-01-21 | Reference manual: fix typo in doc of [tryif/then/else]. | Arnaud Spiwack |
| 2015-01-21 | Embedding the index of the ML tactic entry in the Tacexpr AST. | Pierre-Marie Pédrot |
| 2015-01-20 | Fix a critical bug in machine arithmetic for native compiler. | Maxime Dénès |
| 2015-01-19 | Making unification of LetIn's expressions more consistent (see #3920). | Hugo Herbelin |
| 2015-01-19 | Making unification of LetIn's expressions more consistent (see #3920). | Hugo Herbelin |
| 2015-01-18 | Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it was | Maxime Dénès |
| 2015-01-17 | Merge branch 'v8.5' into trunk | Maxime Dénès |
| 2015-01-17 | Remove dead code. | Maxime Dénès |
| 2015-01-17 | Fix #3379, now that Require inside modules is allowed again. | Maxime Dénès |
| 2015-01-18 | Merge branch '8.5' into trunk | Matthieu Sozeau |
| 2015-01-18 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau |
| 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 |
