coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Réinstallation d'un afficheur de niveau d'imbrication pour le déboggueur de...	herbelin	2003-06-10
*	Ajout FreshId	herbelin	2003-05-24
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	coqide: toolbar/autosave	monate	2003-05-07
*	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin	2003-04-28
*	Localisation des appels de tactiques définies sans arguments	herbelin	2003-04-14
*	Affichage des tactiques en v8	herbelin	2003-04-07
*	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