| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-24 | Removed obsolete option "Legacy Partially Applied Elimination | Hugo Herbelin | |
| Argument" which I used temporarily in a branch to have "destruct eq_dec" working like in v8.4 and not like the "destruct (eq_dec _ _)" of 8.4. I finally made "destruct (eq_dec _ _)" working in 8.5 like "destruct eq_dec" was working in 8.4 (and is still working in 8.5). | |||
| 2015-01-24 | Reference Manual: Documenting new printing of evars and new effect of | Hugo Herbelin | |
| Set Printing Existential Instances (see bug report #3951). | |||
| 2015-01-24 | Equality Schemes options: reverting commit ff9f94634 which is | Hugo Herbelin | |
| obviously inconsistent with the decisions taken in commits 2e8fb20e04da and 0bc569026048 about bugs #2550 and #3606. Now having options Boolean Equality Schemes and Decidable Equality Schemes. | |||
| 2015-01-24 | Isolate a function for printing evar sets. | Hugo Herbelin | |
| 2015-01-24 | Tentative workaround for bug #3798. | Pierre-Marie Pédrot | |
| Ultimately setoid rewrite should be written in the monad to fix it properly. | |||
| 2015-01-23 | Fix previous commit on extraction. | Maxime Dénès | |
| Since name clashes are discovered by side effects, the order of traversal of module structs cannot be changed. | |||
| 2015-01-23 | Typos, grammar, layout in CHANGES (continued). | Hugo Herbelin | |
| 2015-01-23 | Typos, grammar, layout in CHANGES. | Hugo Herbelin | |
| 2015-01-23 | Extraction: fix #3629. | Maxime Dénès | |
| The control flow of extraction is hard to read due to exceptions. When meeting an inlined constant extracted to custom code, they could desynchronize some tables in charge of detecting name clashes, leading to an anomaly. | |||
| 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 ↵ | Arnaud Spiwack | |
| match the overall style. | |||
| 2015-01-21 | Reference Manual/Credits: native compute is a major contribution. | Arnaud Spiwack | |
| It is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two. | |||
| 2015-01-21 | Reference manual/Credits: populate the "various smaller-scale improvements" ↵ | Arnaud Spiwack | |
| part. | |||
| 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 | |
| Fixes #3939. | |||
| 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 | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |