coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Typo	herbelin	2003-10-10
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	Dead of 'a somewhat cryptic module'	herbelin	2003-10-10
*	Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; p...	herbelin	2003-10-10
*	Unification lemInv et lemInv_in	herbelin	2003-10-10
*	Cablage en dur de inversion	herbelin	2003-10-10
*	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin	2003-10-10
*	Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Bug utilisation nametab pour ltac	herbelin	2003-10-08
*	Des abbreviations pour constrintern.ml; generic argument IdentArg	herbelin	2003-10-08
*	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