aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-02-10A few refinements in whodidwhat 8.4.Hugo Herbelin
2015-02-10Fix typeops ignoring results of check functions with let _, and oneMatthieu Sozeau
2015-02-10Add section numbering to the refman PDF. (Fix for bug #2365)Guillaume Melquiond
2015-02-10Prevent Latex from messing with backticks. (Fix for bug #3871)Guillaume Melquiond
2015-02-10Fix documentation of generalize. (Fix for bug #4015)Guillaume Melquiond
2015-02-10Fix some documentation typo.Guillaume Melquiond
2015-02-10Granting wish #4008.Pierre-Marie Pédrot
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