coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	Correction bug NewInduction pour les inductifs de type 'ordinaux'	herbelin	2003-09-23
*	Bug internalisation des Extern: la globalisation doit etre stricte	herbelin	2003-09-23
*	Passage à la V8 par défaut	herbelin	2003-09-22
*	Interface Eauto	herbelin	2003-09-18
*	Indépendance vis à vis de Declare	herbelin	2003-09-12
*	Nettoyage	herbelin	2003-09-11
*	Protection traducteur contre meta de Grammar tactic	herbelin	2003-09-09
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	switching back to old tauto	corbinea	2003-07-03
*	added hints into Ground	corbinea	2003-07-02
*	suppression de newtauto	corbinea	2003-07-02
*	* empty log message *	courant	2003-06-27
*	Une completion de l'interpretation des TacAlias pour la partie interpretable	herbelin	2003-06-25
*	Ground Update.	corbinea	2003-06-20
*	Ajout 'Symmetry in Hyp'	herbelin	2003-06-19
*	Ajout option Local à Hint, Hints et HintDestruct	herbelin	2003-06-14
*	Utilisation de intro_pattern dans NewDestruct/NewInduction	herbelin	2003-06-13
*	Ajout option translate_syntax pour caractériser l'interprétation du traduct...	herbelin	2003-06-12
*	Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...	herbelin	2003-06-10
*	Ground and CCsolve updates	corbinea	2003-05-25
*	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
*	Preservation affichage des ?n en V7	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
*	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