coq - The formal proof system

Age	Commit message (Expand)	Author
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-03-27	appel Zenon sans prelude	filliatr
2006-03-02	tactic haRVey pour appeler haRVey (contrib/dp)	filliatr
2006-03-01	appel de Zenon	filliatr
2006-02-28	* empty log message *	filliatr
2006-02-27	dp: sortie Why	filliatr
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-06-24	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-15	Dp : ajoût des existentiels	coq
2005-06-09	dp: traitement des fixpoints	coq
2005-06-08	traitement des case	coq
2005-05-24	dp: ajout du prouveur Zenon	coq
2005-05-20	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin
2005-04-21	Gestion du forall et envoie d'axiome à la procédure	coq
2005-04-07	dp: traitement des definitions	coq
2005-04-05	Problemes de renommage regles	coq
2005-03-24	symboles de fonctions globaux traites	coq
2005-03-22	Ajout de l'axiome du but prouve par la tactique simplifi	coq
2005-03-18	appel de Simplify depuis Coq	coq
2005-03-16	tactiques prouveurs premier ordre dans contrib/dp/	coq
2005-03-16	nouvelles tactiques pour appeler des procedures de decision du premier ordre	coq