coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Restructuration des procédures de filtrage	herbelin	2003-05-19
*	Separation entre les propositions de syntaxe - suite	herbelin	2003-05-13
*	Enhancement of the Ground tactic, addition of GTauto and GIntuition.	corbinea	2003-05-07
*	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin	2003-04-28
*	Added the Ground tactic.	corbinea	2003-04-25
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey	2003-04-16
*	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
*	code mort	herbelin	2003-04-07
*	Backtrack du commit de Christine, qui posait probleme avec FTC	letouzey	2003-04-03
*	Extension de Replace aux égalités entre preuves	herbelin	2003-04-01
*	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-31
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
*	Fixed Relative names not,iff in Camlp4 quotation.	corbinea	2003-03-28
*	Introducing Christine's Intuition1 and adding some invertible hyps.	corbinea	2003-03-18
*	* empty log message *	barras	2003-03-12
*	Changed Tauto so it displays less 'Unfold not iff'	corbinea	2003-02-26
*	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
*	Suppression de l'élimination des existentiels dans LinearIntuition.	corbinea	2003-02-05
*	Un type "standardisé" pour new_hyp	herbelin	2003-01-25
*	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea	2003-01-23
*	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-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
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Subst sur une hyp qui n'existe pas ne fait pas une anomalie	barras	2003-01-16
*	correction de bug de Subst: ne faisait rien lorsque l'hypothese	barras	2003-01-09
*	Commentaires; optimisation	herbelin	2002-12-30
*	Utilisation du second-ordre avec possibilité de K-rédex dans lemInv	herbelin	2002-12-24
*	code mort	herbelin	2002-12-24
*	Re-essai de forcer le terme réécrit à apparaître dans le but	herbelin	2002-12-23
*	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-21