coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Fix index generation for the pdf document.	gmelquio	2012-09-16
*	Fix failure to compile doc/stdlib/Library.tex.	gmelquio	2012-09-15
*	Port rewrites of tactic documentation from branch 8.4.	gmelquio	2012-09-15
*	Some documentation and cleaning of CList and Util interfaces.	ppedrot	2012-09-15
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Added some tricky tail-rec versions of List functions to CList	ppedrot	2012-09-14
*	Partial revert of Yann commit in order to use CLib.List when opening	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	lib/Pp:	regisgia	2012-09-14
*	kernel/Term:	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Made Pp.std_ppcmds opaque.	ppedrot	2012-09-13
*	Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRS	pboutill	2012-09-12
*	Moved Pp to CLib. In particular, Pp does not depend on CAMLP4/5	ppedrot	2012-09-10
*	Fixed #2893.	ppedrot	2012-09-10
*	Added Print Assumptions command to CoqIDE	ppedrot	2012-09-10
*	When asked for a SearchAbout request, Coq now returns a more precise	ppedrot	2012-09-09
*	Fixed bug #2895	ppedrot	2012-09-09
*	Makefile: revised install-coqide rule	letouzey	2012-09-07
*	Avoid [Loading ML file ...] messages when launching coqtop	letouzey	2012-09-07
*	Coqdoc: fix --utf8 bug for pretty printing	pboutill	2012-09-07
*	Added a comment/uncomment command to CoqIDE	ppedrot	2012-09-06
*	Fix computation of obligations for mutually recursive definitions.	msozeau	2012-09-06
*	Nice output of SearchAbout command in CoqIDE	ppedrot	2012-09-06
*	Obsolete syntax in documentation of Solve Obligation commands.	ppedrot	2012-09-05
*	Rationalized the behaviour of "Next Obligation" and "Admit Obligations"	ppedrot	2012-09-05
*	A few fixes in configure file:	herbelin	2012-09-05
*	Fix coqide compilation with lablgtk 2.16	pboutill	2012-09-04
*	Coqide Fix highlighting of Extraction, Import, Variables	pboutill	2012-09-04
*	test-suite: fix grep rule for output tests	pboutill	2012-09-04
*	test-suite uses coqtop instead of coqtop.byte	pboutill	2012-09-04
*	Erase %.vo dependency to the phony target states	pboutill	2012-09-04
*	In the output tests, ignore dynlink messages	letouzey	2012-08-24
*	correct some ends of .mllib files (avoid a broken tolink.ml)	letouzey	2012-08-24
*	Use fully-qualified Coq.Init.Prelude when starting coqtop	letouzey	2012-08-24
*	Fix Extraction Implicit on axioms.	aspiwack	2012-08-24
*	Experimental support for a comment in the files' preamble in extraction.	aspiwack	2012-08-24
*	Add option Set/Unset Extraction Conservative Types.	aspiwack	2012-08-24
*	Better highlighting of strings in coqide.	aspiwack	2012-08-24
*	Assumption commands are now displayed as unsafe in Coqide.	aspiwack	2012-08-24
*	Modification of the unjustified tag.	aspiwack	2012-08-24
*	Correcting a comment in pattern-matching compilation.	aspiwack	2012-08-24
*	test-suite: Local Tactic Notation is now legal since r15731	letouzey	2012-08-23
*	CHANGES: document the end of states/initial.coq and coqtop.opt	letouzey	2012-08-23
*	Remove a script unused since 2006 (cf commit r8626)	letouzey	2012-08-23
*	myocamlbuild : fixes for new printing directory + sourceview for coqide	letouzey	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
*	No need anymore to refer to COQLIB in ocamldebug-coq	letouzey	2012-08-23