coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Nouvelle en-tête	herbelin	2004-07-16
*	more evar stuff	corbinea	2004-06-28
*	effective evar refining	corbinea	2004-06-26
*	Déplacement définition intro_pattern_expr dans Genarg	herbelin	2004-03-01
*	bugs avec Pose et Assert	barras	2004-01-09
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Added Instantiate ... in	corbinea	2003-11-06
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	* empty log message *	barras	2003-03-12
*	Un type "standardisé" pour new_hyp	herbelin	2003-01-25
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin	2002-10-21
*	NewDestruct/NewInduction acceptent l'option "using"	herbelin	2002-10-21
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin	2001-06-25
*	entetes	filliatr	2001-03-15
*	Ajout du langage de tactiques	delahaye	2000-05-03
*	Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations	filliatr	1999-11-24
*	modules Indrec, Tacentries, Hiddentac	filliatr	1999-11-23