coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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