coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec alpha-c...	herbelin	2003-10-21
*	Correction bug FreshId	herbelin	2003-10-21
*	Globalisation des hints autorewrite	herbelin	2003-10-20
*	Extension de l'utilisation de contradiction	herbelin	2003-10-19
*	Extension de Contradiction au cas d'hypotheses ~A et A dans le contexte	herbelin	2003-10-18
*	subst marche dans les deux sens	filliatr	2003-10-17
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	Un Try supplementaire utile pour la compatibilite, car bring_hyps dans genera...	herbelin	2003-10-13
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
*	Uniformisation comportement decompEq pour corriger un bug introduit dans le I...	herbelin	2003-10-11
*	Bug calcul du nom de la premiere equation	herbelin	2003-10-11
*	Death of 'a somewhat cryptic module'	herbelin	2003-10-11
*	Death of 'a somewhat cryptic module'	herbelin	2003-10-11
*	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