coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Pushing lazy lists into Ltac. Now, the control flow is explicit	ppedrot	2013-05-28
*	Code cleaning in Matching.	ppedrot	2013-05-24
*	Fixing ocamldoc compilation.	ppedrot	2013-05-06
*	Matching patterns: fixed allow_partial_app which was not working on	herbelin	2013-04-17
*	Modulification of identifier	ppedrot	2012-12-14
*	Adapt pieces of code needing -rectypes	letouzey	2012-10-06
*	Updating headers.	herbelin	2012-08-08
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	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
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Added support for subterm matching in SearchAbout.	herbelin	2008-12-29
*	Quelques modifications autour du filtrage Ltac:	herbelin	2008-07-16
*	Add possibility to match on defined hypotheses, using brackets to	msozeau	2008-06-16
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ...	herbelin	2004-09-25
*	Nouvelle en-tête	herbelin	2004-07-16
*	Correction bug 371 (sub_match retournait des instances non closes)	herbelin	2003-12-16
*	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