aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-02-10Test for bug #4012.Pierre-Marie Pédrot
2015-02-10More expressive API for tclWITHHOLES.Pierre-Marie Pédrot
2015-02-10Making undo/redo atomic in CoqIDE.Pierre-Marie Pédrot
2015-02-10Revert "Removing spurious tclWITHHOLES."Pierre-Marie Pédrot
2015-02-09Fix bug #4014.Pierre-Marie Pédrot
2015-02-07STM: tolerate simple side effects in async proofs (Close: 4006)Enrico Tassi
2015-02-07Fixing bug #4009.Pierre-Marie Pédrot
2015-02-06More efficient Richpp.Pierre-Marie Pédrot
2015-02-05Windows: open .vo files in binary modeEnrico Tassi
2015-02-05Fix some documentation typos.Guillaume Melquiond
2015-02-05Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)Enrico Tassi
2015-02-05Windows installer cleanupEnrico Tassi
2015-02-05Marshal.from_string on 32 bit systems use tmpfile if needed (Close: 3968)Enrico Tassi
2015-02-05Properly set module names in presence of -Q. (Fix for bug #3958)Guillaume Melquiond
2015-02-04Detecting automatically whether .opt versions of ocaml executables exist;Hugo Herbelin
2015-02-04Optimized Import/Export the same way as Require Import/Export wasHugo Herbelin
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