coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...	herbelin	2003-06-10
*	Amélioration affichage locations; prise en compte variables dans lettac; ajo...	herbelin	2003-05-24
*	Réparation d'un bug de backtracking qui lui-même succédait à une ineffica...	herbelin	2003-05-22
*	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
*	Separation entre les propositions de syntaxe - suite	herbelin	2003-05-13
*	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
*	Bug: lookup inapproprie dans subst_tactic	herbelin	2003-04-14
*	Relachement globalisation Unfold en usage interactif	herbelin	2003-04-10
*	Trop de restriction pour les TacDef	herbelin	2003-04-10
*	Prise en compte des variables de grammaires de tactiques et dédollarisation ...	herbelin	2003-04-08
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Ajout d'un message à FailTac; localisation des appels à des tactiques défi...	herbelin	2003-03-31
*	* empty log message *	barras	2003-03-12
*	Correction d'un bug introduit dans le backtracking d'occurrence	delahaye	2003-02-13
*	Chargement dynamique de .cma	delahaye	2003-02-13
*	Debugger plus informatif	delahaye	2003-02-13
*	Mauvais environnement d'évaluation pour les globaux	herbelin	2003-01-22
*	Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur	herbelin	2003-01-21
*	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-20
*	Utilisation d'une exception 'catchable'	herbelin	2003-01-19
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
*	Traitement spécial pour les types à l'internalisation	herbelin	2002-12-15
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	Re-ajout constrIn	herbelin	2002-11-14
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	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
*	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