| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-01-13 | More documentation of the Local Definitions and Axioms. | Pierre-Marie Pédrot | |
| 2015-01-13 | More in CHANGES about local definitions | Pierre-Marie Pédrot | |
| 2015-01-13 | TCs: Properly handle Hint Extern with conclusions of the form _ -> _ | Matthieu Sozeau | |
| in typeclasses eauto, remaining compatible with eauto and still producing eta-reduced applications for Hint Resolves. Fixes bug #3794. | |||
| 2015-01-13 | Fix test-suite file, we were testing that no anomaly was raised | Matthieu Sozeau | |
| and this is the case now. | |||
| 2015-01-13 | Update hash of cic.mli in checker/values.ml, | Matthieu Sozeau | |
| letting make validate progress. | |||
| 2015-01-13 | Fix bug when discharging universe constraints coming from variables | Matthieu Sozeau | |
| into monomorphic constants, which was still using the de Bruijn encoding Bug revealed by discharging of hidden internal monomorphic definition in otherwise polymorphic developments. Makes coqchk work on Hurkens again. | |||
| 2015-01-13 | Fix issue in printing due to de Bruijn bug when constructing compatibility | Matthieu Sozeau | |
| constr for primitive records (not used anywhere else than printing). Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT. Also add some minor fixes in detyping and pretty printing related to universes. | |||
| 2015-01-12 | typo in coqide compilation rules after -thread requirement | Pierre Boutillier | |
| 2015-01-12 | Derive -> derive occurences | Pierre Boutillier | |
| 2015-01-12 | Coq_makefile erases native compiler files | Pierre Boutillier | |
| 2015-01-12 | fixup to vi -> vio renaming | Enrico Tassi | |
| 2015-01-12 | Whodidwhat-8.5: a global pass | Arnaud Spiwack | |
| Updating my own work and others when I could think of them. | |||
| 2015-01-12 | whodidwhat-8.5: typo. | Arnaud Spiwack | |
| 2015-01-12 | Add -no-native-compiler flag to list dumped by --help. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |