coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Amélioration de DiscrR	desmettr	2003-01-20
*	* empty log message *	herbelin	2003-01-20
*	Protection contre les noms de tactiques inconnus; restriction exceptions ratt...	herbelin	2003-01-20
*	Utilisation de 'Recursive' pour les tactiques récursives	herbelin	2003-01-20
*	deplacement du test 'il reste des preuves en cours'	filliatr	2003-01-20
*	Utilisation de 'Recursive' pour les tactiques récursives	herbelin	2003-01-20
*	maj	filliatr	2003-01-20
*	MAJ	herbelin	2003-01-20
*	Petits bugs	herbelin	2003-01-20
*	Tests ltac	herbelin	2003-01-19
*	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin	2003-01-19
*	Simplification de Simplify (plus de ())	herbelin	2003-01-19
*	MAJ Ltac	herbelin	2003-01-19
*	Utilisation d'une exception 'catchable'	herbelin	2003-01-19
*	Clear sur hypothese non definie	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Ajout pptac	herbelin	2003-01-19
*	Erreur sur precedent commit	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Localisation	herbelin	2003-01-19
*	Rétablissement pr_pattern	herbelin	2003-01-19
*	maj	filliatr	2003-01-18
*	msg Failtac; echec -batch s'il reste des preuves	filliatr	2003-01-17
*	V7.4	mohring	2003-01-17
*	* empty log message *	mohring	2003-01-17
*	Version V7.4	mohring	2003-01-17
*	Mise a jour pour distrib	mohring	2003-01-17
*	* empty log message *	mohring	2003-01-17
*	Optimisations pour Sup et RCompute	desmettr	2003-01-17
*	maj	filliatr	2003-01-17
*	Bugs affichage	herbelin	2003-01-16
*	* empty log message *	herbelin	2003-01-16
*	Subst sur une hyp qui n'existe pas ne fait pas une anomalie	barras	2003-01-16
*	Ajout de RCompute	desmettr	2003-01-16
*	Ajout de la tactique Sup	desmettr	2003-01-16
*	* empty log message *	desmettr	2003-01-16
*	renommage de TAF.v en MVT.v	desmettr	2003-01-16
*	-emacs: plus de prompt entre les lignes	filliatr	2003-01-16
*	Correction d'un petit bug dans Sup0	desmettr	2003-01-16
*	Renommage de RealsB en Rbase	desmettr	2003-01-16
*	Renommage de Rbase.v en RIneq.v	desmettr	2003-01-16
*	maj	filliatr	2003-01-16
*	Problème de désynchronisation des variables du type et du corps d'un point-...	herbelin	2003-01-15
*	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin	2003-01-15
*	Bug en présence de let-in	herbelin	2003-01-15
*	Nouvelle interprétation des nombres réels	desmettr	2003-01-15
*	Bug en présence de let-in	herbelin	2003-01-15
*	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin	2003-01-15
*	patch configure (V Aymeric)	filliatr	2003-01-13