aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Tentative workaround for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-24
* Fix previous commit on extraction.Gravatar Maxime Dénès2015-01-23
* Typos, grammar, layout in CHANGES (continued).Gravatar Hugo Herbelin2015-01-23
* Typos, grammar, layout in CHANGES.Gravatar Hugo Herbelin2015-01-23
* Extraction: fix #3629.Gravatar Maxime Dénès2015-01-23
* Add the possibility of defining opaque terms with program.Gravatar mlasson2015-01-21
* Reference Manual/Credits: expand the paragraph on the new proof engine to mat...Gravatar Arnaud Spiwack2015-01-21
* Reference Manual/Credits: native compute is a major contribution.Gravatar Arnaud Spiwack2015-01-21
* Reference manual/Credits: populate the "various smaller-scale improvements" p...Gravatar Arnaud Spiwack2015-01-21
* Reference Manual/Credits: remove a duplicate.Gravatar Arnaud Spiwack2015-01-21
* Reference manual: pass over the credit section for English.Gravatar Arnaud Spiwack2015-01-21
* Reference manual: fix typo in doc of [tryif/then/else].Gravatar Arnaud Spiwack2015-01-21
* Fix a critical bug in machine arithmetic for native compiler.Gravatar Maxime Dénès2015-01-20
* Making unification of LetIn's expressions more consistent (see #3920).Gravatar Hugo Herbelin2015-01-19
* Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it wasGravatar Maxime Dénès2015-01-18
* 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
* 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
* Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Gravatar Matthieu Sozeau2015-01-16
* 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
* Add a (by default deactivated) option to force typeclass resolution toGravatar Matthieu Sozeau2015-01-15
* Expand Credits for 8.5 and doc on universesGravatar Matthieu Sozeau2015-01-15
* Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Gravatar Matthieu Sozeau2015-01-15
* Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-15
* Update header of CHANGES.Gravatar Maxime Dénès2015-01-15
* Remove left-over dead code in previous commit.Gravatar Maxime Dénès2015-01-15
* Make -print-mod-uid accept a list of files.Gravatar Maxime Dénès2015-01-15
* Mention CHANGES file in COMPATIBILITY.Gravatar Maxime Dénès2015-01-15
* Mention guard condition in CHANGES.Gravatar Maxime Dénès2015-01-15
* Make installation of native files more robust.Gravatar Maxime Dénès2015-01-15
* coq_makefile installs native filesGravatar Pierre Boutillier2015-01-15
* Always build (even when -coqide no) and install idetoploopGravatar Pierre Boutillier2015-01-15
* Hugo put me in credits, but I was already there :)Gravatar Maxime Dénès2015-01-15
* Tentatively updating credits while remaining brief.Gravatar Hugo Herbelin2015-01-15
* Makefile: install ide/*langGravatar Enrico Tassi2015-01-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 18:31:49 +0000