coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	tactics/eqdecide.ml4: avoid a useless argument in decideEquality	glondu	2010-12-24
*	Remove the two-argument variant of "decide equality"	glondu	2010-12-23
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Added two new introduction patterns with the following temptative syntaxes:	herbelin	2009-06-07
*	Cleaning/uniformizing the interface of tacticals.mli	herbelin	2009-03-14
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	Extension syntaxique de rewrite in: au lieu de pouvoir faire	letouzey	2006-05-02
*	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin	2006-03-22
*	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin	2006-01-28
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Types inductifs parametriques	mohring	2005-11-02
*	Nouvelle en-tête	herbelin	2004-07-16
*	Restructuration des procédures de filtrage	herbelin	2003-05-19
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey	2003-04-16
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...	herbelin	2002-06-05
*	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...	herbelin	2002-06-05
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29