aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-01-29Fix index of reference manual.Guillaume Melquiond
2015-01-29An update on INSTALL.ide.Hugo Herbelin
2015-01-29Removing outdated INSTALL.macosx file; instructions are more likely toHugo Herbelin
2015-01-29Extra check at the INSTALL file.Hugo Herbelin
2015-01-29Remove spurious "Loading ML file" and "<W> Grammar extension" from the refere...Guillaume Melquiond
2015-01-29Remove some "Warning:" from the reference manual.Guillaume Melquiond
2015-01-29Prevent spurious warnings about Arguments.Guillaume Melquiond
2015-01-29Made the CoqIDE progress gutter clickable.Pierre-Marie Pédrot
2015-01-29Fix some typos in the documentation.Guillaume Melquiond
2015-01-29Fix some broken Coq scripts in the reference manual.Guillaume Melquiond
2015-01-28Fixing bug #3931.Pierre-Marie Pédrot
2015-01-28Several reproduction cases for the test suite.Xavier Clerc
2015-01-28Several reproduction cases for the test suite.Xavier Clerc
2015-01-27Adding a test for bug #3957.Pierre-Marie Pédrot
2015-01-27Tentative fix for bug #3957.Pierre-Marie Pédrot
2015-01-27Fixed a wrong warning in coq_makefile.Pierre Courtieu
2015-01-27Fixed a wrong warning in coq_makefile.Pierre Courtieu
2015-01-27Allow -type-in-type to be an option also for coqc.Daniel R. Grayson
2015-01-27Doc: Overfull lines in chapter on Canonical Structures.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 19:46:44 +0000