aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-02-11Win: use .exe extension for the ocaml compiler (Close 3572)Enrico Tassi
2015-02-11STM: is Flags.async_proofs_full then always delegateEnrico Tassi
2015-02-11Fixing bug #4019, and checker blow-up at once.Pierre-Marie Pédrot
2015-02-11Clarifying the implementation of universe hashconsing.Pierre-Marie Pédrot
2015-02-11Adding a statistic function on hashconsing tables.Pierre-Marie Pédrot
2015-02-11Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-11Adding a test-suite for tactic notation naming.Pierre-Marie Pédrot
2015-02-11Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307)Guillaume Melquiond
2015-02-11Adding test for bug #3900.Pierre-Marie Pédrot
2015-02-11Fixing bug #3900.Pierre-Marie Pédrot
2015-02-11Reinstauring backtrace display in CoqIDE.Pierre-Marie Pédrot
2015-02-10Avoid html markup inside tex files and fix url.Guillaume Melquiond
2015-02-10Run coqdoc on the .v files from the plugins directory. (Fix for bug #2195)Guillaume Melquiond
2015-02-10Fixing #4001 (missing type constraints when building return clause of match).Hugo Herbelin
2015-02-10Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coq...Hugo Herbelin
2015-02-10Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...Hugo Herbelin
2015-02-10Fixing #4018 (uncaught exception on non-equality in intros [=]).Hugo Herbelin
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