aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-01-25Equipping extended maps with fold operator defined for any monad.Pierre-Marie Pédrot
2015-01-25Merge branch 'v8.5' into trunk.Pierre-Marie Pédrot
2015-01-25Made replacing of text in CoqIDE atomic w.r.t. the undo/redo.Pierre-Marie Pédrot
2015-01-25Fixing bug #3947.Pierre-Marie Pédrot
2015-01-25Adding a proper interface to Newring.Pierre-Marie Pédrot
2015-01-25Test for bug #3798.Pierre-Marie Pédrot
2015-01-24Doc: Fixing some compilation problems with chapter CanonicalHugo Herbelin
2015-01-24Updating CHANGES (grammar, thanks to AS for pointing it out) +Hugo Herbelin
2015-01-24Removed obsolete option "Legacy Partially Applied EliminationHugo Herbelin
2015-01-24Reference Manual: Documenting new printing of evars and new effect ofHugo Herbelin
2015-01-24Equality Schemes options: reverting commit ff9f94634 which isHugo Herbelin
2015-01-24Isolate a function for printing evar sets.Hugo Herbelin
2015-01-24Tentative workaround for bug #3798.Pierre-Marie Pédrot
2015-01-23Splitting ML tactics in one function per grammar entry.Pierre-Marie Pédrot
2015-01-23Fix previous commit on extraction.Maxime Dénès
2015-01-23Typos, grammar, layout in CHANGES (continued).Hugo Herbelin
2015-01-23Typos, grammar, layout in CHANGES.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 23:20:10 +0000