coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Added a new exception for already declared Schemes,	vsiles	2010-04-27
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin	2010-04-19
*	Util: remove list_split_at which is a clone of list_chop	letouzey	2010-04-16
*	Look for csdp in $PATH at runtime, remove -csdpdir configure option	glondu	2010-04-11
*	infrastructure for safe marshal-based IPC	vgross	2010-03-23
*	Util.lowercase_unicode: avoid creating the segmenttree each time (speeds some...	letouzey	2010-02-15
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	* Segmenttree: New. A very simple implementation of segment trees.	regisgia	2010-01-08
*	Generic support for open terms in tactics	herbelin	2009-12-21
*	* Rewrite [classify_unicode] using standard unicode tables.	regisgia	2009-12-20
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	Document Generalizable Variables, and change syntax to	msozeau	2009-11-15
*	Make usages of the Obj module explicit	glondu	2009-11-13
*	Experiment propagation of implicit arguments and arguments scope for	herbelin	2009-11-12
*	Revision 12439 continued, printing part (notations to names behave	herbelin	2009-10-29
*	Fix bug in dnet.ml, which missed some results when filtering one term against...	puech	2009-10-29
*	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau	2009-10-28
*	New functors for gmap and gset.	soubiran	2009-10-26
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Changed the way to support compatibility with previous versions.	herbelin	2009-10-04
*	Fixed a hole in glob_tactic that allowed some Ltac code to refer to	herbelin	2009-09-26
*	Add the option to automatically introduce variables declared before the	msozeau	2009-09-22
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	Tried to make F1 documentation tool working in CoqIDE.	herbelin	2009-08-14
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Use camlp4 to accept some specific non-exhaustive patterns in groebner	letouzey	2009-07-20
*	Fixed anomaly when trying to load non existing file starting with "./" or "../".	herbelin	2009-07-08
*	Accept more Unicode symbols	glondu	2009-06-10
*	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin	2009-05-09
*	- Cleaning (unification of ML names, removal of obsolete code,	herbelin	2009-04-27
*	comparison functions on lists and arrays	barras	2009-04-16
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	A first pearl found by the Oug analyzer: there were two list_map_i in Util	letouzey	2009-04-08
*	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey	2009-03-20
*	Timeout message was not always displayed	barras	2009-03-04
*	Heavy modifications on the widget and edition tab creation mechanism.	vgross	2009-03-02
*	Gestion des espaces dans les noms + guess_coqlib sous Windows	notin	2009-02-11
*	Fix d'un problème lors de l'appel à coqtop avec un chemin relatif	notin	2009-02-11
*	memoized is_ground_env	barras	2009-02-09
*	- Fixed various Overfull in documentation.	herbelin	2009-01-27
*	Petit nettoyage faisant suite au commit #11847 .	aspiwack	2009-01-23
*	Util.split_at : for quadratic to linear complexity	letouzey	2009-01-22
*	Experimental file commited by mistake, sorry.	herbelin	2009-01-19
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
*	DISCLAIMER	puech	2009-01-17