| Age | Commit message (Expand) | Author |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi |
| 2014-07-24 | Forgot to add a Universes.v.tex as a target. | Matthieu Sozeau |
| 2014-07-24 | fixup fakeide test-suite | Pierre Boutillier |
| 2014-07-22 | A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundle | Pierre Boutillier |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi |
| 2014-06-25 | cut toploop(s) out of coqtop: now they are loaded dynamically | Enrico Tassi |
| 2014-05-05 | Fix install target in Makefile after 6acf543800fe176ca7d47ef7165ebc14588efb6f. | Maxime Dénès |
| 2014-04-25 | Adding a stm/ folder, as asked during last workgroup. It was essentially moving | Pierre-Marie Pédrot |
| 2014-03-24 | Revert "Makefile: the initial build of grammar.cma is now directory-driven" | Pierre Letouzey |
| 2014-03-07 | Compiling coqc in "tools" target. | Pierre-Marie Pédrot |
| 2014-03-02 | Makefile: the initial build of grammar.cma is now directory-driven | Pierre Letouzey |
| 2014-02-24 | Fix coqide build under MacOS | Pierre Boutillier |
| 2014-01-26 | Spawn: managed processes | Enrico Tassi |
| 2014-01-05 | refman: fist stab at Asynchronous Proofs | Enrico Tassi |
| 2013-12-16 | A few fixes to the build system (mostly for ocamlbuild) | Pierre Letouzey |
| 2013-12-04 | Documentation of the Derive plugin. | Arnaud Spiwack |
| 2013-12-04 | Derive plugin. | Arnaud Spiwack |
| 2013-11-29 | First stab at documenting Canonical Structures | Enrico Tassi |
| 2013-09-06 | Moving Searchstack to CStack, and normalizing names a bit. | ppedrot |
| 2013-08-08 | Searchable stack data structure | gareuselesinge |
| 2013-05-06 | New module Xml_printer (dual to Xml_parser) | gareuselesinge |
| 2013-04-18 | coqc and coqmktop migrated in tools/, get rid of scripts/ subdir | letouzey |
| 2013-04-17 | Coqmktop: dynlink is now mandatory due to Maxime's native-compiler | letouzey |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-10 | Tiny fix of r16049 | pboutill |
| 2012-10-29 | Allow running coq-tex in win32 (fix #2921) | letouzey |
| 2012-10-15 | Makefiles: Only -I required dirs (config, lib, ide) when compiling coqide | pboutill |
| 2012-10-04 | Moved Compat to parsing. This permits to break the dependency of the | ppedrot |
| 2012-09-15 | Port rewrites of tactic documentation from branch 8.4. | gmelquio |
| 2012-09-12 | Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRS | pboutill |
| 2012-08-23 | No more states/initial.coq, instead coqtop now requires Prelude.vo | letouzey |
| 2012-08-23 | No more coqtop.opt, produce directly a coqtop binary | letouzey |
| 2012-08-23 | configure: get rid of the -src option and of ${COQSRC} | letouzey |
| 2012-08-23 | Port from 8.4 branch some build fixes concerning win32 : | letouzey |
| 2012-08-22 | Do not forget to build the unicode libraries, necessary to compile and launch... | msozeau |
| 2012-08-08 | Fixup for macOS 10.8 & Ocaml 4.0 | pboutill |
| 2012-07-05 | Legacy Ring and Legacy Field migrated to contribs | letouzey |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-20 | Install compat5 module with grammar.cma | pboutill |
| 2012-05-29 | place all pretty-printing files in new dir printing/ | letouzey |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-05-29 | Vernacexpr is now a mli-only file, locality stuff now in locality.ml | letouzey |
| 2012-05-23 | Revert copy/pasted function in to minilib thanks to clib.cma | pboutill |
| 2012-05-15 | Makefile: Really avoid locales in $(DATE) | letouzey |
| 2012-05-10 | Addedum to documentation of bullets: I now use the dedicated coq_example | aspiwack |
| 2012-04-17 | Remove the Dp plugin. | gmelquio |
| 2012-04-12 | lib directory is cut in 2 cma. | pboutill |
| 2012-03-14 | Final part of moving Program code inside the main code. Adapted add_definitio... | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-01-13 | Added a Btauto plugin, that solves boolean tautologies. | ppedrot |