aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Embedding the index of the ML tactic entry in the Tacexpr AST.Gravatar Pierre-Marie Pédrot2015-01-21
* Making unification of LetIn's expressions more consistent (see #3920).Gravatar Hugo Herbelin2015-01-19
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-01-17
|\
| * Remove dead code.Gravatar Maxime Dénès2015-01-17
| * Fix #3379, now that Require inside modules is allowed again.Gravatar Maxime Dénès2015-01-17
* | Merge branch '8.5' into trunkGravatar Matthieu Sozeau2015-01-18
|\|
* | Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-18
* | Univs: Complete documentation in refman.Gravatar Matthieu Sozeau2015-01-18
* | Partially revert "Forbid Require inside interactive modules and module types."Gravatar Maxime Dénès2015-01-18
* | Revert "Adapting two files from test-suite to now forbidden Require's in modu...Gravatar Maxime Dénès2015-01-18
* | Revert "Update test for #3363 now that Require is forbidden inside modules."Gravatar Maxime Dénès2015-01-18
* | Revert "Fix files in test-suite having to do with Require inside modules."Gravatar Maxime Dénès2015-01-18
* | Avoid compilation warning... might not be the best fix though.Gravatar Matthieu Sozeau2015-01-18
* | Univs: Fix alias computation for VMs, computation of normal form ofGravatar Matthieu Sozeau2015-01-18
* | Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-18
* | coq_makefile: install also .v and .globGravatar Enrico Tassi2015-01-18
* | Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Gravatar Matthieu Sozeau2015-01-18
* | vm_printers: fix compilationGravatar Enrico Tassi2015-01-18
* | Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-18
* | Minor fixes to the refman credits to be continued.Gravatar Matthieu Sozeau2015-01-18
* | Move explanations about primitive projections to the manual.Gravatar Matthieu Sozeau2015-01-18
* | Add a (by default deactivated) option to force typeclass resolution toGravatar Matthieu Sozeau2015-01-18
* | Expand Credits for 8.5 and doc on universesGravatar Matthieu Sozeau2015-01-18
* | Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Gravatar Matthieu Sozeau2015-01-18
* | Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-18
* | Update header of CHANGES.Gravatar Maxime Dénès2015-01-18
| * There was one more universe needed due to the use of now non-universe-polymor...Gravatar Matthieu Sozeau2015-01-18
| * Back to 4 expected universes.Gravatar Matthieu Sozeau2015-01-17
| * Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
| * Univs: Complete documentation in refman.Gravatar Matthieu Sozeau2015-01-17
| * Partially revert "Forbid Require inside interactive modules and module types."Gravatar Maxime Dénès2015-01-17
| * Revert "Adapting two files from test-suite to now forbidden Require's in modu...Gravatar Maxime Dénès2015-01-17
| * Revert "Update test for #3363 now that Require is forbidden inside modules."Gravatar Maxime Dénès2015-01-17
| * Revert "Fix files in test-suite having to do with Require inside modules."Gravatar Maxime Dénès2015-01-17
| * Avoid compilation warning... might not be the best fix though.Gravatar Matthieu Sozeau2015-01-17
| * Univs: Fix alias computation for VMs, computation of normal form ofGravatar Matthieu Sozeau2015-01-17
| * Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
| * coq_makefile: install also .v and .globGravatar Enrico Tassi2015-01-16
| * Documenting the removal of coercions between sig, sigT, sig2,Gravatar Hugo Herbelin2015-01-16
* | Documenting the removal of coercions between sig, sigT, sig2,Gravatar Hugo Herbelin2015-01-16
* | Add two lemmas about firstn to the List standard library.Gravatar Sébastien Hinderer2015-01-16
* | Lemmas related to the firstn function over lists.Gravatar Sébastien Hinderer2015-01-16
* | ListSet: follow-up of Sebastien's last commitGravatar Pierre Letouzey2015-01-16
* | Work in progress on listset.Gravatar Sébastien Hinderer2015-01-16
| * Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Gravatar Matthieu Sozeau2015-01-16
* | Added stuff about -I -Q -R in COMPATIBILTY.Gravatar Pierre Courtieu2015-01-15
| * vm_printers: fix compilationGravatar Enrico Tassi2015-01-15
| * Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
| * Minor fixes to the refman credits to be continued.Gravatar Matthieu Sozeau2015-01-15
| * Move explanations about primitive projections to the manual.Gravatar Matthieu Sozeau2015-01-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 21:22:11 +0000