coq - The formal proof system

Age	Commit message (Expand)	Author
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-20	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-19	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-18	maj	filliatr
2003-01-17	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-16	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