coq - The formal proof system

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