| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-19 | Making unification of LetIn's expressions more consistent (see #3920). | Hugo Herbelin | |
| Unifying two let-in's expresions syntactically is a heuristic (compared to performing the zeta-reduction). This heuristic was requiring unification of types which is too strong for the heuristic to work uniformly since the types might only be related modulo subtyping. The patch is to remove the unification of types, which allows then to have the heuristic work uniformly on the bodies. On the other side, I hope it does not loose (still heuristical) unifications compared to before (presumably, since instantiating the evars in the body will induce constraints for solving potential evars in the types of the let-in bodies, but this would need a proof). Anyway, it is not about correction, it is about a heuristic, which maybe done too early actually. | |||
| 2015-01-18 | Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it was | Maxime Dénès | |
| actually calling the VM at Qed time. | |||
| 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 | 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 | 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 | 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 | |
| 2015-01-15 | Remove typeclass opaque directive, some proofs in the stdlib rely on it ↵ | Matthieu Sozeau | |
| being transparent | |||
| 2015-01-15 | 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-15 | Update header of CHANGES. | Maxime Dénès | |
| 2015-01-15 | Remove left-over dead code in previous commit. | Maxime Dénès | |
| 2015-01-15 | Make -print-mod-uid accept a list of files. | Maxime Dénès | |
| Solves an efficiency problem in Makefiles generated by coq_makefile. | |||
| 2015-01-15 | Mention CHANGES file in COMPATIBILITY. | Maxime Dénès | |
| 2015-01-15 | Mention guard condition in CHANGES. | Maxime Dénès | |
| 2015-01-15 | Make installation of native files more robust. | Maxime Dénès | |
| 2015-01-15 | coq_makefile installs native files | Pierre Boutillier | |
| 2015-01-15 | Always build (even when -coqide no) and install idetoploop | Pierre Boutillier | |
| So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed) | |||
| 2015-01-15 | Hugo put me in credits, but I was already there :) | Maxime Dénès | |
| 2015-01-15 | Tentatively updating credits while remaining brief. | Hugo Herbelin | |
| 2015-01-14 | Makefile: install ide/*lang | Enrico Tassi | |
| 2015-01-14 | coq_makefile: chmod 755 on toplopp cmxs | Enrico Tassi | |
| 2015-01-14 | CoqIDE: a Make file to build coqidetop toploop | Enrico Tassi | |
| 2015-01-14 | Reference manual: I had previously omitted the syntax entry for [> t1|…|tn]. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document tryif/then/else. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document multimatch. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: try and improve documentation for Ltac's match. | Arnaud Spiwack | |
| In particular document the "once" behaviour. | |||
| 2015-01-14 | Reference manual: try and improve the documentation of lazymatch. | Arnaud Spiwack | |
| In particular try to avoid the use of the word "backtracking" which refers to too many things. | |||
| 2015-01-14 | Reference manual: document gfail. | Arnaud Spiwack | |
| 2015-01-14 | CHANGES: my recent updates to Ltac. | Arnaud Spiwack | |
| - gfail - multimatch - tryif/then/else | |||
| 2015-01-13 | Bump version and magic numbers in configure. | Maxime Dénès | |
| 2015-01-13 | Made -print-mod-uid more silent and robust. | Maxime Dénès | |
| This is a follow-up on Pierre's 5d80a385. | |||
| 2015-01-13 | Refresh some copyright headers. | Maxime Dénès | |
| 2015-01-13 | Native compiler: if debug flag not present, remove .native files. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |