coq - The formal proof system

Age	Commit message (Expand)	Author
2002-12-15	Pas d'associativite pour =_D	herbelin
2002-12-15	Evaluation paresseuse de l'affichage du debug	herbelin
2002-12-14	maj	filliatr
2002-12-13	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-12	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-11	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-10	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-09	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-07	Compatibilité times1	herbelin