aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-02-04Fixing bug #3996.Pierre-Marie Pédrot
2015-02-04More efficient implementation of Richpp.Pierre-Marie Pédrot
2015-02-04Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-04CThread: workaround for threads lockup on windwos made more aggressiveEnrico Tassi
2015-02-04Nativelib: catch Unix_error (like no ocamlopt found)Enrico Tassi
2015-02-03Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Enrico Tassi
2015-02-03Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-03spit module path using / as directory separatorEnrico Tassi
2015-02-02Removing dead code.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-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-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-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-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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 23:23:20 +0000