coq - The formal proof system

Age	Commit message (Expand)	Author
2003-01-20	Mauvaise interprétatin de IdentArgType	herbelin
2003-01-20	Protection contre les noms de tactiques inconnus; restriction exceptions ratt...	herbelin
2003-01-20	Petits bugs	herbelin
2003-01-19	Utilisation d'une exception 'catchable'	herbelin
2003-01-19	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin
2003-01-19	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin
2003-01-16	Subst sur une hyp qui n'existe pas ne fait pas une anomalie	barras
2003-01-09	correction de bug de Subst: ne faisait rien lorsque l'hypothese	barras
2002-12-30	Commentaires; optimisation	herbelin
2002-12-24	Utilisation du second-ordre avec possibilité de K-rédex dans lemInv	herbelin
2002-12-24	code mort	herbelin
2002-12-23	Re-essai de forcer le terme réécrit à apparaître dans le but	herbelin
2002-12-21	Backtrack sur la tentative d'interdire les K-abstractions dans l'unification	herbelin
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-19	suite du commit precedent	barras
2002-12-17	nouveau Subst:	barras
2002-12-15	Traitement spécial pour les types à l'internalisation	herbelin
2002-12-12	Ajout du vernac Proof with	gregoire
2002-12-10	Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)	herbelin
2002-12-09	Option pour rendre les vérifications du refiner optionnelle	herbelin
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-11-14	Re-ajout constrIn	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-14	JMeq now treated as an equality by tactics.	courant
2002-11-06	Raffinement de l'heuristique d'unification dans sig_clausale_forme	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-10-23	Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local	herbelin
2002-10-22	Correction d'une incompatibilité de nommage introduite lors du commit préc�...	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-10-14	Réparation bug Inversion (#212)	herbelin
2002-10-09	retour en arriere concernant la recherche d'occurence modulo expansion des le...	barras
2002-10-08	Subst ne fait pas clear sur x:=e	filliatr
2002-10-01	Oops...	coq
2002-10-01	Table fonctionnelle dans autorewrite	coq
2002-10-01	Vraie substitutivite de autohints	coq
2002-10-01	bug de noms long pour eqT.	clrenard
2002-09-29	Que des niveaux d'univers frais dans le type des constantes globales	herbelin
2002-09-27	passage a ocaml 3.06	herbelin
2002-09-16	Subst (tout court)	filliatr
2002-09-11	tactique Subst x1 ... xn	filliatr
2002-09-09	Code mort de AutoRewrite	herbelin
2002-08-16	correction de bugs:	barras
2002-08-13	AutoRewrite substitutive...	coq
2002-08-13	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-07-30	Branchement de Assert, Pose et LetTac sur l'algo de création de noms	herbelin
2002-07-19	correction bugs Tauto	courant
2002-07-17	tactique Subst	filliatr