coq - The formal proof system

Age	Commit message (Expand)	Author
2002-12-16	Petit netoyage des open's et commentaires	coq
2002-12-16	maj	filliatr
2002-12-15	MAJ	herbelin
2002-12-15	Une entrée spéciale "annot" pour les piquants	herbelin
2002-12-15	Ajout syntaxe '>'	herbelin
2002-12-15	Traitement spécial pour les types à l'internalisation	herbelin
2002-12-15	Ajout "Locate Notation"	herbelin
2002-12-15	Prise en compte des scopes traversés dans les notations	herbelin
2002-12-15	Meilleure factorisation des entrées NEXT internes	herbelin
2002-12-15	Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxe	herbelin
2002-12-15	Pas de 0 dans positive	herbelin
2002-12-15	Ajout syntaxe '>'	herbelin
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