coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin	2008-12-19
*	Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of	herbelin	2008-12-10
*	profondeur maximale	filliatr	2008-09-10
*	debug et nouvelles commandes Dp_prelude et Dp_predefined	filliatr	2008-05-13
*	Test que la bibliothèque ZArith est chargée lors d'un appel à simplify, er...	notin	2008-04-22
*	tactique gappa	filliatr	2008-04-17
*	flottants	filliatr	2008-04-16
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	tactique gappa	filliatr	2008-03-19
*	tactique gappa	filliatr	2008-03-14
*	tactique Gappa : mise en place	filliatr	2008-03-11
*	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin	2007-11-08
*	bugs dp	filliatr	2007-11-06
*	traces Ergo	filliatr	2007-03-20
*	encodage des types	filliatr	2007-02-14
*	tactique yices	filliatr	2007-02-14
*	Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouent	herbelin	2007-01-22
*	typo malencontreuse	filliatr	2006-12-21
*	contrib/dp: tactique ergo (voir ergo.lri.fr)	filliatr	2006-12-15
*	contrib/dp	filliatr	2006-12-08
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	appel Zenon sans prelude	filliatr	2006-03-27
*	tactic haRVey pour appeler haRVey (contrib/dp)	filliatr	2006-03-02
*	appel de Zenon	filliatr	2006-03-01
*	* empty log message *	filliatr	2006-02-28
*	dp: sortie Why	filliatr	2006-02-27
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Dp: ajout d'abstraction aux applications de fonction non premier ordre	coq	2005-06-24
*	dp: ajout des prédicats de sortes	coq	2005-06-24
*	Dp : ajoût des existentiels	coq	2005-06-15
*	dp: traitement des fixpoints	coq	2005-06-09
*	traitement des case	coq	2005-06-08
*	dp: ajout du prouveur Zenon	coq	2005-05-24
*	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin	2005-05-20
*	Gestion du forall et envoie d'axiome à la procédure	coq	2005-04-21
*	dp: traitement des definitions	coq	2005-04-07
*	Problemes de renommage regles	coq	2005-04-05
*	symboles de fonctions globaux traites	coq	2005-03-24
*	Ajout de l'axiome du but prouve par la tactique simplifi	coq	2005-03-22
*	appel de Simplify depuis Coq	coq	2005-03-18
*	tactiques prouveurs premier ordre dans contrib/dp/	coq	2005-03-16
*	nouvelles tactiques pour appeler des procedures de decision du premier ordre	coq	2005-03-16