coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	petite erreur de syntaxe	barras	2002-05-14
*	ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewrite	barras	2002-05-14
*	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr	2002-05-07
*	lemmes plus_O_n et plus_Sn_m (pour Yves)	filliatr	2002-05-07
*	Uniformisation (Qed/Save et Implicits Arguments)	herbelin	2002-04-17
*	Doc	herbelin	2002-02-22
*	Uniformisation des theoremes dans Set et Type (def. de Acc_rect et	barras	2002-02-19
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
*	Syntaxe IF then else au lieu de either and_then or_else	barras	2002-02-14
*	changement generation de schema d'elimination, False_rec est primitif, Constr...	mohring	2002-01-31
*	modification de la definition des def inductives unitaires et autorisation d'...	mohring	2002-01-29
*	Modifs incongrues dans le précédent commit	herbelin	2002-01-10
*	MAJ des Id pour coqweb	herbelin	2002-01-09
*	Suppression d'Export redondants	herbelin	2001-11-14
*	Suppression de Logic_Type.sigT, redondant avec Specif.sigT	herbelin	2001-10-24
*	and_rec redondant	letouzey	2001-09-27
*	Transparent	barras	2001-09-20
*	Deplacement des setoides.	clrenard	2001-09-19
*	Modification de l'emplacement des fichiers pour les setoides.	clrenard	2001-09-18
*	Fin de la modif Exc/option	mohring	2001-08-30
*	ajout option , Exc --> option, et lemmes dans les theories	mohring	2001-08-29
*	Expérimentation de NewDestruct et parfois NewInduction	herbelin	2001-08-05
*	Correction d'un bug du pretty-print	clrenard	2001-05-29
*	Modification pour passage p-automates	mohring	2001-05-15
*	documentation automatique de la bibliothèque standard	filliatr	2001-04-11
*	Introduction d'une preuve de False_rec	mohring	2001-03-30
*	entetes	filliatr	2001-03-15
*	Bug d'affichage à cause des << ... >>	herbelin	2000-12-21
*	separation calcul des implicites et declaration des constantes / inductifs / ...	filliatr	2000-11-21
*	Bug dans la règle de syntaxe de ex2	herbelin	2000-11-20
*	Modification de la table des tactic Definitions pour eviter l'ecriture	mohring	2000-11-07
*	Changement/extension dans les noms de parseurs de Grammar	herbelin	2000-11-07
*	Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...	herbelin	2000-10-18
*	Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...	herbelin	2000-07-28
*	Bug affichage Error et Value	herbelin	2000-04-30
*	t -> $t dans regle grammaire EX	filliatr	2000-03-10
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21
*	Renommage command en constr	herbelin	2000-01-07
*	erreurs de syntax :$	filliatr	1999-12-16
*	- méthode load sur les Hints	filliatr	1999-12-13
*	fichiers prelude Coq	filliatr	1999-12-13