coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Install compat5 module with grammar.cma	pboutill	2012-06-20
*	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-29
*	Revert copy/pasted function in to minilib thanks to clib.cma	pboutill	2012-05-23
*	Makefile: Really avoid locales in $(DATE)	letouzey	2012-05-15
*	Addedum to documentation of bullets: I now use the dedicated coq_example	aspiwack	2012-05-10
*	Remove the Dp plugin.	gmelquio	2012-04-17
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Added a Btauto plugin, that solves boolean tautologies.	ppedrot	2012-01-13
*	fix Makefile.common handling of -byte-only	gareuselesinge	2011-12-06
*	Moving XML handling to lib directory	ppedrot	2011-11-24
*	Added XML dependencies into Makefile	ppedrot	2011-11-06
*	Added XML manipulation tools to compilation chain	ppedrot	2011-11-06
*	Various fixes in the Makefiles	letouzey	2011-09-17
*	make world now builds fake_ide (to please coq-bench)	letouzey	2011-09-06
*	A new mechanism to handle errors.	aspiwack	2011-05-13
*	remove useless dependancy for csdpcert	fbesson	2011-05-09
*	Ide: restaure compilation of ide/macjokes.c removed by mistake	letouzey	2011-03-28
*	Ide: more reorganisation and cleanup	letouzey	2011-03-25
*	Ide: stronger separation from coqtop	letouzey	2011-03-23
*	Revert "syntax for exponents"	glondu	2011-02-25
*	syntax for exponents	pottier	2011-02-22
*	Add a test for sorting all universes of stdlib	glondu	2011-01-25
*	MacOS integration	pboutill	2011-01-07
*	Coqide is not built with coqmktop any more	pboutill	2011-01-07
*	First release of Vector library.	pboutill	2010-12-10
*	Move stuff about positive into a distinct PArith subdir	letouzey	2010-11-02
*	dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...	letouzey	2010-09-24
*	Fixed compilation with statically-linked plugins (the decl_mode	herbelin	2010-07-07
*	Backport from trunk to 8.3 of modifications on groebner/nsatz	herbelin	2010-06-22
*	Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_int	letouzey	2010-06-04
*	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier	2010-06-03
*	Extraction: start of a support library	letouzey	2010-06-02
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	"make source-doc" builds documentation of mli in html and pdf at	pboutill	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	New model for user-driven translation of tokens in coqdoc	herbelin	2010-04-06
*	Définition de GRAMMARCMA: parsing/grammar.cma n'était plus installé, ce qu...	notin	2010-03-19
*	Makefile: some more cleanup	letouzey	2010-03-05
*	Makefile: no more separate stages	letouzey	2010-03-04
*	Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)	letouzey	2010-03-04
*	make init + NMake.v/NMake_gen.v	notin	2010-01-26
*	* Segmenttree: New. A very simple implementation of segment trees.	regisgia	2010-01-08
*	* Rewrite [classify_unicode] using standard unicode tables.	regisgia	2009-12-20
*	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey	2009-12-09