aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-01-25Adding a proper interface to Newring.Pierre-Marie Pédrot
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
2015-01-23Merge branch 'v8.5' into trunkMaxime Dénès
2015-01-23Extraction: fix #3629.Maxime Dénès
2015-01-21Add the possibility of defining opaque terms with program.mlasson
2015-01-21Reference Manual/Credits: expand the paragraph on the new proof engine to mat...Arnaud Spiwack
2015-01-21Reference Manual/Credits: native compute is a major contribution.Arnaud Spiwack
2015-01-21Reference manual/Credits: populate the "various smaller-scale improvements" p...Arnaud Spiwack
2015-01-21Reference Manual/Credits: remove a duplicate.Arnaud Spiwack
2015-01-21Reference manual: pass over the credit section for English.Arnaud Spiwack
2015-01-21Reference manual: fix typo in doc of [tryif/then/else].Arnaud Spiwack
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-20Fix a critical bug in machine arithmetic for native compiler.Maxime Dénès
2015-01-19Making unification of LetIn's expressions more consistent (see #3920).Hugo Herbelin
2015-01-19Making unification of LetIn's expressions more consistent (see #3920).Hugo Herbelin
2015-01-18Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it wasMaxime Dénès
2015-01-17Merge branch 'v8.5' into trunkMaxime 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-18Merge branch '8.5' into trunkMatthieu Sozeau
2015-01-18Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-28 17:10:04 +0000