coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Ajout d'un message à FailTac	herbelin	2003-03-31
*	Réparation bug de l'unification. En effet, avant l'instanciation d'une evar	clrenard	2003-03-28
*	* empty log message *	barras	2003-03-12
*	Debugger plus informatif	delahaye	2003-02-13
*	Bug Rename	herbelin	2003-02-08
*	Pour satisfaire ProofGeneral	coq	2003-01-31
*	Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur	herbelin	2003-01-21
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Erreur sur precedent commit	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Amélioration choix des noms dans abstract_list_all	herbelin	2002-12-30
*	code mort	herbelin	2002-12-24
*	Tentative d'interdire les K-abstractions si allow_K est faux et le	herbelin	2002-12-23
*	Cas motif universel	herbelin	2002-12-22
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
*	code mort	herbelin	2002-12-21
*	Prise en compte des coercions dans les 'with' bindings	herbelin	2002-12-20
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
*	suite du commit precedent	barras	2002-12-19
*	Compensation de suppression betaiota de type_of (suite)	herbelin	2002-12-13
*	Compensation de suppression betaiota de type_of (suite)	herbelin	2002-12-12
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Compensation de suppression betaiota de type_of	herbelin	2002-12-11
*	Option pour rendre les vérifications du refiner optionnelle	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-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	simplification common_ancestor	courant	2002-11-13
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	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
*	Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage	herbelin	2002-10-13
*	retour en arriere concernant la recherche d'occurence modulo expansion des le...	barras	2002-10-09
*	Vraie substitutivite de autohints	coq	2002-10-01
*	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin	2002-08-13
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Ajout d'un point d'entree pour exporter les arbres de preuves en XML	herbelin	2002-07-24
*	MAJ commentaires	herbelin	2002-07-23
*	Protection contre l'encapsulage de FailError dans Exc_located (sinon, par exe...	herbelin	2002-07-11
*	Commentaires	herbelin	2002-06-14
*	Bug non vérification non redondance par Cut	herbelin	2002-06-13
*	Déplacement de proofs vers tactics	herbelin	2002-05-29
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Réorganisation des tclTHEN (cf dev/changements.txt)	herbelin	2002-05-29
*	Fichier des expressions de tactiques	herbelin	2002-05-29
*	Ajout de Eval, Inst et Check	delahaye	2002-05-27
*	Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de	herbelin	2002-05-15
*	Finalement VTactic est gardé pour y plonger les tactiques ML, le	herbelin	2002-05-15