| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-01-17 | Remove dead code. | Maxime Dénès | |
| Follow-up on Matthieu's d030ce0721. | |||
| 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 | |
| printing functions touched in the kernel). | |||
| 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 | |
| This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put back in place the Requires inside modules that were found in the std lib. Conflicts: kernel/safe_typing.ml | |||
| 2015-01-18 | Revert "Adapting two files from test-suite to now forbidden Require's in ↵ | Maxime Dénès | |
| modules." This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e. | |||
| 2015-01-18 | Revert "Update test for #3363 now that Require is forbidden inside modules." | Maxime Dénès | |
| This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d. | |||
| 2015-01-18 | Revert "Fix files in test-suite having to do with Require inside modules." | Maxime Dénès | |
| This reverts commit a7ed77403cd15ba1cc2c05f2b6193b46f0028eda. | |||
| 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 | |
| match predicates for vm_compute and compile polymorphic definitions to constant code. Add univscompute test-suite file testing VM computations in presence of polymorphic universes. | |||
| 2015-01-18 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès | |
| One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem. | |||
| 2015-01-18 | coq_makefile: install also .v and .glob | Enrico Tassi | |
| This is useful for PIDE based interfaces, since they can build hyperlinks out of .glob files and let the user jump to the corresponding .v files | |||
| 2015-01-18 | Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _" | Matthieu Sozeau | |
| Not supposed to be part of 8.5beta. This reverts commit 74682bb27da074fedc115238f3085baaccf12d73. | |||
| 2015-01-18 | vm_printers: fix compilation | Enrico Tassi | |
| 2015-01-18 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau | |
| definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions. | |||
| 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 | |
| respect dependencies between typeclass goals, trying to solve the least dependent ones first. | |||
| 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 ↵ | Matthieu Sozeau | |
| being transparent | |||
| 2015-01-18 | Optionally allow eta-conversion during unification for type classes. | Matthieu Sozeau | |
| Off by default as it can be backwards-incompatible (e.g. produces loop in the library without an additional Typeclasses Opaque directive in RelationPairs). | |||
| 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 ↵ | Matthieu Sozeau | |
| non-universe-polymorphic ID, fixing the script results in 3 universes for the stdlib again. | |||
| 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 | |
| printing functions touched in the kernel). | |||
| 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 | |
| This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put back in place the Requires inside modules that were found in the std lib. Conflicts: kernel/safe_typing.ml | |||
| 2015-01-17 | Revert "Adapting two files from test-suite to now forbidden Require's in ↵ | Maxime Dénès | |
| modules." This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e. | |||
| 2015-01-17 | Revert "Update test for #3363 now that Require is forbidden inside modules." | Maxime Dénès | |
| This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d. | |||
| 2015-01-17 | Revert "Fix files in test-suite having to do with Require inside modules." | Maxime Dénès | |
| This reverts commit a7ed77403cd15ba1cc2c05f2b6193b46f0028eda. | |||
| 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 | |
| match predicates for vm_compute and compile polymorphic definitions to constant code. Add univscompute test-suite file testing VM computations in presence of polymorphic universes. | |||
| 2015-01-17 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès | |
| One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem. | |||
| 2015-01-16 | coq_makefile: install also .v and .glob | Enrico Tassi | |
| This is useful for PIDE based interfaces, since they can build hyperlinks out of .glob files and let the user jump to the corresponding .v files | |||
| 2015-01-16 | Documenting the removal of coercions between sig, sigT, sig2, | Hugo Herbelin | |
| etc. (source of incompatibility). | |||
| 2015-01-16 | Documenting the removal of coercions between sig, sigT, sig2, | Hugo Herbelin | |
| etc. (source of incompatibility). | |||
| 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 | |
| More results on set_remove, in particular explicit the NoDup pre-condition. Show that NoDup is preserved by other operations. | |||
| 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 | |
| Not supposed to be part of 8.5beta. This reverts commit 74682bb27da074fedc115238f3085baaccf12d73. | |||
| 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 | |
| definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions. | |||
| 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 | |
| respect dependencies between typeclass goals, trying to solve the least dependent ones first. | |||
| 2015-01-15 | Expand Credits for 8.5 and doc on universes | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |