coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Pas d'associativite pour =_D	herbelin	2002-12-15
*	Evaluation paresseuse de l'affichage du debug	herbelin	2002-12-15
*	maj	filliatr	2002-12-14
*	Compensation de suppression betaiota de type_of (suite)	herbelin	2002-12-13
*	debut de parcours des modules	letouzey	2002-12-13
*	une branche de case inutile	letouzey	2002-12-13
*	possibilité de faire Print M avec M module ou modtype au lieu de Print Modul...	letouzey	2002-12-13
*	correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...	letouzey	2002-12-13
*	maj	filliatr	2002-12-13
*	Compensation de suppression betaiota de type_of (suite)	herbelin	2002-12-12
*	* empty log message *	gregoire	2002-12-12
*	Ajout du vernac Proof with	gregoire	2002-12-12
*	Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...	desmettr	2002-12-12
*	maj	filliatr	2002-12-12
*	Essai de hconsing local au declarations	herbelin	2002-12-11
*	Compensation de suppression betaiota de type_of	herbelin	2002-12-11
*	maj	filliatr	2002-12-11
*	Bugs divers	herbelin	2002-12-10
*	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin	2002-12-10
*	Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)	herbelin	2002-12-10
*	Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse la	herbelin	2002-12-10
*	Compatibilite times1 (suite)	herbelin	2002-12-10
*	Normalisation des types (fait avant dans Typing)	herbelin	2002-12-10
*	Protection contre les variables anonymes dans match_aconstr	herbelin	2002-12-10
*	Déplacement du hash-consing vers declare.ml	herbelin	2002-12-10
*	Hash-consing dès la lib_stk	herbelin	2002-12-10
*	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin	2002-12-10
*	Commentaires	herbelin	2002-12-10
*	Avertissement plus clair	herbelin	2002-12-10
*	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin	2002-12-10
*	maj	filliatr	2002-12-10
*	Corrections de gestion des univers et modules + meilleure gestions des noms...	coq	2002-12-09
*	Ajoute le bon traitement pour Ring, Locate, Comments	bertot	2002-12-09
*	Add an example with Ring.	bertot	2002-12-09
*	setoids dans noreal	letouzey	2002-12-09
*	Take notations into account: numbers and the CNotation operator.	bertot	2002-12-09
*	Option pour rendre les vérifications du refiner optionnelle	herbelin	2002-12-09
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	Problèmes et améliorations divers affichage	herbelin	2002-12-09
*	Essai suppression nf_betaiota dans type_of	herbelin	2002-12-09
*	Nouvelle preuve de times_convert pour nouvelle définition de times	herbelin	2002-12-09
*	Problèmes et améliorations affichage; Changement Simpl	herbelin	2002-12-09
*	Problèmes et améliorations divers affichage	herbelin	2002-12-09
*	Option pour rendre les vérifications du refiner optionnelle	herbelin	2002-12-09
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	Code mort ?	herbelin	2002-12-09
*	pp	letouzey	2002-12-09
*	petit bug	letouzey	2002-12-09
*	chamboulement du codage des indcutifs extraits; deplacements des tables; ...	letouzey	2002-12-09
*	Compatibilité times1	herbelin	2002-12-07