coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout recarg_length	herbelin	2003-11-18
*	Un nouveau lemme redondant ...	herbelin	2003-11-18
*	Deplacement ZERO_le_inj dans Zorder	herbelin	2003-11-18
*	Utilisation de la date cvs dans l'en-tete si make.result existe	herbelin	2003-11-18
*	* empty log message *	filliatr	2003-11-18
*	maj	filliatr	2003-11-18
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
*	Bug affichage Hint Extern	herbelin	2003-11-17
*	Inteprétation des idents filtrés liants dans constrintern.ml (plus robuste)	herbelin	2003-11-17
*	Un ident filtre est liant seulement si une variable deja liee (sinon bug dans...	herbelin	2003-11-17
*	maj	filliatr	2003-11-17
*	Bug filtrage pour inversion notation	herbelin	2003-11-16
*	Amelioration du message d'erreur en cas de tentative d'instanciation	clrenard	2003-11-15
*	Bug nommage destruct	herbelin	2003-11-15
*	Meilleure solution pour la compatibilite	herbelin	2003-11-15
*	Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar	herbelin	2003-11-15
*	Ajout Print Implicit avec depliage du type	herbelin	2003-11-15
*	MAJ date	herbelin	2003-11-14
*	Pour les .v8	herbelin	2003-11-14
*	Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robuste	herbelin	2003-11-14
*	MAJ	herbelin	2003-11-14
*	Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_base	herbelin	2003-11-14
*	Conflit renommage	herbelin	2003-11-14
*	cosmetique	herbelin	2003-11-14
*	Presentation	herbelin	2003-11-14
*	Oublis dans les rennomages	herbelin	2003-11-14
*	Check bavard meme en mode silencieux, car on l'a voulu	herbelin	2003-11-14
*	Ordre standard pour l'associativite	herbelin	2003-11-14
*	Quelques oublis pour que les notations marchent bien	herbelin	2003-11-14
*	Compatibilite %T	herbelin	2003-11-14
*	Bug implicit arguments	herbelin	2003-11-14
*	Correction chemin de Z	herbelin	2003-11-14
*	Automatisation de la traduction de iff_trans; renommage IF	herbelin	2003-11-14
*	Backtrack sur Peano	herbelin	2003-11-14
*	Nouveaux lemmes 'canoniques'; compatibilite	herbelin	2003-11-14
*	Suppression renommages dans Peano	herbelin	2003-11-14
*	Bug parsing cast	herbelin	2003-11-14
*	maj	filliatr	2003-11-14
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13
*	Traduction Print Grammar	herbelin	2003-11-13
*	Oubli report Nul/Pos	herbelin	2003-11-13
*	Niveau V8	herbelin	2003-11-13
*	Fermeture de la section maintenant necessaire	herbelin	2003-11-13
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Passage a un SStream predicatif	herbelin	2003-11-13
*	MAJ	herbelin	2003-11-13
*	Require	herbelin	2003-11-13
*	qq petit ajouts à Zdiv	letouzey	2003-11-13
*	maj	filliatr	2003-11-13
*	MAJ INZ	herbelin	2003-11-12