aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-01-18Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it wasMaxime Dénès
2015-01-17Remove dead code.Maxime Dénès
2015-01-17Fix #3379, now that Require inside modules is allowed again.Maxime Dénès
2015-01-18There was one more universe needed due to the use of now non-universe-polymor...Matthieu Sozeau
2015-01-17Back to 4 expected universes.Matthieu Sozeau
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Univs: Complete documentation in refman.Matthieu Sozeau
2015-01-17Partially revert "Forbid Require inside interactive modules and module types."Maxime Dénès
2015-01-17Revert "Adapting two files from test-suite to now forbidden Require's in modu...Maxime Dénès
2015-01-17Revert "Update test for #3363 now that Require is forbidden inside modules."Maxime Dénès
2015-01-17Revert "Fix files in test-suite having to do with Require inside modules."Maxime Dénès
2015-01-17Avoid compilation warning... might not be the best fix though.Matthieu Sozeau
2015-01-17Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-16coq_makefile: install also .v and .globEnrico Tassi
2015-01-16Documenting the removal of coercions between sig, sigT, sig2,Hugo Herbelin
2015-01-16Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Matthieu Sozeau
2015-01-15vm_printers: fix compilationEnrico Tassi
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-15Minor fixes to the refman credits to be continued.Matthieu Sozeau
2015-01-15Move explanations about primitive projections to the manual.Matthieu Sozeau
2015-01-15Add a (by default deactivated) option to force typeclass resolution toMatthieu Sozeau
2015-01-15Expand Credits for 8.5 and doc on universesMatthieu Sozeau
2015-01-15Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Matthieu Sozeau
2015-01-15Optionally allow eta-conversion during unification for type classes.Matthieu Sozeau
2015-01-15Update header of CHANGES.Maxime Dénès
2015-01-15Remove left-over dead code in previous commit.Maxime Dénès
2015-01-15Make -print-mod-uid accept a list of files.Maxime Dénès
2015-01-15Mention CHANGES file in COMPATIBILITY.Maxime Dénès
2015-01-15Mention guard condition in CHANGES.Maxime Dénès
2015-01-15Make installation of native files more robust.Maxime Dénès
2015-01-15coq_makefile installs native filesPierre Boutillier
2015-01-15Always build (even when -coqide no) and install idetoploopPierre Boutillier
2015-01-15Hugo put me in credits, but I was already there :)Maxime Dénès
2015-01-15Tentatively updating credits while remaining brief.Hugo Herbelin
2015-01-14Makefile: install ide/*langEnrico Tassi
2015-01-14coq_makefile: chmod 755 on toplopp cmxsEnrico Tassi
2015-01-14CoqIDE: a Make file to build coqidetop toploopEnrico Tassi
2015-01-14Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].Arnaud Spiwack
2015-01-14Reference manual: document tryif/then/else.Arnaud Spiwack
2015-01-14Reference manual: document multimatch.Arnaud Spiwack
2015-01-14Reference manual: try and improve documentation for Ltac's match.Arnaud Spiwack
2015-01-14Reference manual: try and improve the documentation of lazymatch.Arnaud Spiwack
2015-01-14Reference manual: document gfail.Arnaud Spiwack
2015-01-14CHANGES: my recent updates to Ltac.Arnaud Spiwack
2015-01-13Bump version and magic numbers in configure.Maxime Dénès
2015-01-13Made -print-mod-uid more silent and robust.Maxime Dénès
2015-01-13Refresh some copyright headers.Maxime Dénès
2015-01-13Native compiler: if debug flag not present, remove .native files.Maxime Dénès
2015-01-13More documentation of the Local Definitions and Axioms.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 18:03:17 +0000