coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin	2003-10-30
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Changement de la politique de V8only: V8only tout seul signifie	herbelin	2003-09-21
*	Mise en conformite de la precedence du '-' unaire avec celle de Notations (su...	herbelin	2003-05-21
*	Mise en conformite de la precedence du '-' unaire avec celle de Notations	herbelin	2003-05-21
*	* empty log message *	barras	2003-03-12
*	Remplacement Grammar par Notation	herbelin	2002-12-02
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-12-02
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
*	Modification de l'emplacement des fichiers pour les setoides.	clrenard	2001-09-18
*	Passage au nouveau Destruct	herbelin	2001-08-07
*	Expérimentation de NewDestruct et parfois NewInduction	herbelin	2001-08-05
*	Ajout des fichiers pour le Ring pour setoides	clrenard	2001-07-10