coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Renommages dans PartSum	desmettr	2003-01-22
*	Bug 'with Module' corrige	coq	2003-01-22
*	Bug precedence	herbelin	2003-01-22
*	petit bug pp haskell	letouzey	2003-01-22
*	maj	filliatr	2003-01-22
*	Extraction des modules, enfin !	letouzey	2003-01-22
*	id_of_msid en plus	letouzey	2003-01-22
*	Adaptation à la nouvelle sémantique plus uniforme de "Match term"	herbelin	2003-01-21
*	Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur	herbelin	2003-01-21
*	portabilite	doligez	2003-01-21
*	Renommage dans MVT	desmettr	2003-01-21
*	MAJ dans Exp_prop	desmettr	2003-01-21
*	Renommage dans Binomial.v	desmettr	2003-01-21
*	Binome.v -> Binomial.v	desmettr	2003-01-21
*	Binome.v -> Binomial.v	desmettr	2003-01-21
*	MAJ ArithProp	desmettr	2003-01-21
*	Renommage dans AltSeries.v	desmettr	2003-01-21
*	Renommage dans Alembert.v	desmettr	2003-01-21
*	Quelques améliorations	desmettr	2003-01-21
*	Suppression de INR2 / Conséquence logique de la nouvelle représentation des...	desmettr	2003-01-21
*	Quelques optimisations...	desmettr	2003-01-21
*	Make sure pcoq will also display hypotheses with a value.	bertot	2003-01-21
*	Add a few operators in the new version of xlate.ml and make sure	bertot	2003-01-21
*	maj	filliatr	2003-01-21
*	Mauvaise interprétatin de IdentArgType	herbelin	2003-01-20
*	Cgt définition de plat	desmettr	2003-01-20
*	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