coq - The formal proof system

Age	Commit message (Expand)	Author
2003-05-25	Ground and CCsolve updates	corbinea
2003-05-24	Amélioration affichage locations; prise en compte variables dans lettac; ajo...	herbelin
2003-05-22	Réparation d'un bug de backtracking qui lui-même succédait à une ineffica...	herbelin
2003-05-22	Preservation affichage des ?n en V7	herbelin
2003-05-21	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-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-05-19	Restructuration des procédures de filtrage	herbelin
2003-05-13	Separation entre les propositions de syntaxe - suite	herbelin
2003-05-07	Enhancement of the Ground tactic, addition of GTauto and GIntuition.	corbinea
2003-04-28	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin
2003-04-25	Added the Ground tactic.	corbinea
2003-04-16	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey
2003-04-14	Localisation des appels de tactiques définies sans arguments	herbelin
2003-04-14	Bug: lookup inapproprie dans subst_tactic	herbelin
2003-04-10	Relachement globalisation Unfold en usage interactif	herbelin
2003-04-10	Trop de restriction pour les TacDef	herbelin
2003-04-08	Prise en compte des variables de grammaires de tactiques et dédollarisation ...	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-04-07	code mort	herbelin
2003-04-03	Backtrack du commit de Christine, qui posait probleme avec FTC	letouzey
2003-04-01	Extension de Replace aux égalités entre preuves	herbelin
2003-03-31	Ajout d'un message à FailTac	herbelin
2003-03-31	Ajout d'un message à FailTac; localisation des appels à des tactiques défi...	herbelin
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
2003-03-29	eq fusionne avec eqT et devient par défaut sur Type,	herbelin
2003-03-28	notations <>, Assumption avec existentiel, replace term	mohring
2003-03-28	Fixed Relative names not,iff in Camlp4 quotation.	corbinea
2003-03-18	Introducing Christine's Intuition1 and adding some invertible hyps.	corbinea
2003-03-12	* empty log message *	barras
2003-02-26	Changed Tauto so it displays less 'Unfold not iff'	corbinea
2003-02-13	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-05	Suppression de l'élimination des existentiels dans LinearIntuition.	corbinea
2003-01-25	Un type "standardisé" pour new_hyp	herbelin
2003-01-23	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea
2003-01-22	Mauvais environnement d'évaluation pour les globaux	herbelin
2003-01-22	Correction bug réecriture à la racine pour le sétoide Prop.	clrenard
2003-01-21	Plus du tout de backtracking dans "Match term"; vrai Exit dans débogueur	herbelin
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