coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin	2002-10-21
*	NewDestruct/NewInduction acceptent l'option "using"	herbelin	2002-10-21
*	L'application de ltac attend une référence; meilleure protection contre	herbelin	2002-10-14
*	correction de bugs:	barras	2002-08-16
*	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin	2002-08-13
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Bug dans la globalisation des arguments de tactiques primitives	herbelin	2002-07-16
*	Que la localisation des erreurs pour les tactiques atomiques marche	herbelin	2002-07-11
*	Hack pour autoriser les $n dans les Grammar tactic	herbelin	2002-07-03
*	Réparation de l'interprétation des fermetures (sans casser Field!)	herbelin	2002-06-13
*	Ajout coercion constr vers hyp quantifiée	herbelin	2002-06-06
*	Les VContext ne sont plus des fermetures (temporaire)	delahaye	2002-05-31
*	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin	2002-05-30
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29