aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-01-18Univs: Complete documentation in refman.Matthieu Sozeau
2015-01-18Partially revert "Forbid Require inside interactive modules and module types."Maxime Dénès
2015-01-18Revert "Adapting two files from test-suite to now forbidden Require's in modu...Maxime Dénès
2015-01-18Revert "Update test for #3363 now that Require is forbidden inside modules."Maxime Dénès
2015-01-18Revert "Fix files in test-suite having to do with Require inside modules."Maxime Dénès
2015-01-18Avoid compilation warning... might not be the best fix though.Matthieu Sozeau
2015-01-18Univs: Fix alias computation for VMs, computation of normal form ofMatthieu Sozeau
2015-01-18Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-18coq_makefile: install also .v and .globEnrico Tassi
2015-01-18Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Matthieu Sozeau
2015-01-18vm_printers: fix compilationEnrico Tassi
2015-01-18Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-18Minor fixes to the refman credits to be continued.Matthieu Sozeau
2015-01-18Move explanations about primitive projections to the manual.Matthieu Sozeau
2015-01-18Add a (by default deactivated) option to force typeclass resolution toMatthieu Sozeau
2015-01-18Expand Credits for 8.5 and doc on universesMatthieu Sozeau
2015-01-18Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Matthieu Sozeau
2015-01-18Optionally allow eta-conversion during unification for type classes.Matthieu Sozeau
2015-01-18Update header of CHANGES.Maxime Dénès
2015-01-16Documenting the removal of coercions between sig, sigT, sig2,Hugo Herbelin
2015-01-16Add two lemmas about firstn to the List standard library.Sébastien Hinderer
2015-01-16Lemmas related to the firstn function over lists.Sébastien Hinderer
2015-01-16ListSet: follow-up of Sebastien's last commitPierre Letouzey
2015-01-16Work in progress on listset.Sébastien Hinderer
2015-01-15Added stuff about -I -Q -R in COMPATIBILTY.Pierre Courtieu
2015-01-15Revert "Bump version and magic numbers in configure."Maxime Dénès
2015-01-15Merge branch 'v8.5' into trunkMaxime 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-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-15Hugo put me in credits, but I was already there :)Maxime Dénès
2015-01-15Makefile: install ide/*langEnrico Tassi
2015-01-15coq_makefile: chmod 755 on toplopp cmxsEnrico Tassi
2015-01-15CoqIDE: a Make file to build coqidetop toploopEnrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 21:27:43 +0000