coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Removing useless tactic arguments, and using generic arguments	ppedrot	2013-06-27
*	Now, idtac closures use maps instead of association list.	ppedrot	2013-06-22
*	Hiding tactic value representations.	ppedrot	2013-06-10
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (tactics)	ppedrot	2012-11-25
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	place all files specific to camlp4 syntax extensions in grammar/	letouzey	2012-05-29
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey	2012-05-15
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Noise for nothing	pboutill	2012-03-02
*	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau	2012-01-31
*	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau	2012-01-28
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24
*	Applying Tom Prince's patch to support parametric "constructor n" in	herbelin	2011-10-25
*	Simplify tactic(_)-bound arguments in TACTIC EXTEND rules	glondu	2010-09-30
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	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
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	Fix tauto no longer failing after commit 12077; appropriate error	herbelin	2009-04-10
*	Turning tauto into a classical tautology prover as soon as classical	herbelin	2009-04-09
*	Solves some warning and hides some not-bad ones in doc. It remains a	herbelin	2009-01-29
*	- Fixed bugs and compatibilities issues in	herbelin	2008-12-30
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	More compatibility fixes, revert the tauto fix that prevented	msozeau	2008-07-25
*	Tauto breaking not only binary "conjunctions" seems like a bad idea	msozeau	2008-07-24
*	A try at allowing matching on applications as a binary syntax node by default.	msozeau	2008-07-22
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Modifications diverses et variées :	herbelin	2008-03-30
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Nouvelle en-tête	herbelin	2004-07-16
*	* empty log message *	barras	2003-12-23
*	petits changements de syntaxe	barras	2003-11-12