coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	Passage à la V8 par défaut	herbelin	2003-09-22
*	switching back to old tauto	corbinea	2003-07-03
*	added hints into Ground	corbinea	2003-07-02
*	* empty log message *	courant	2003-06-27
*	Preservation affichage des ?n en V7	herbelin	2003-05-22
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Fixed Relative names not,iff in Camlp4 quotation.	corbinea	2003-03-28
*	Introducing Christine's Intuition1 and adding some invertible hyps.	corbinea	2003-03-18
*	Changed Tauto so it displays less 'Unfold not iff'	corbinea	2003-02-26
*	Suppression de l'élimination des existentiels dans LinearIntuition.	corbinea	2003-02-05
*	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea	2003-01-23
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	correction bugs Tauto	courant	2002-07-19
*	Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3\|- ?]	corbinea	2002-07-17
*	Correction bug Tauto : la regle pour (A->B)->C echouait quand C etait	courant	2002-07-15
*	Nettoyage	herbelin	2002-05-30
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29