coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Un axiome en attendant la mise a jour de la preuve de times_convert	herbelin	2002-12-06
*	Amélioration sensible de l'efficacité de Zmult et times	herbelin	2002-12-06
*	Amélioration sensible de l'efficacité de la multiplication	herbelin	2002-12-06
*	maj	filliatr	2002-12-06
*	Ajout affichage fconstr	herbelin	2002-12-05
*	reorganisation des recherches de ref dans ml_decl	letouzey	2002-12-05
*	code cleanup (+ debut de commencement de modules)	letouzey	2002-12-05
*	des Set et des Map en plus	letouzey	2002-12-05
*	Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...	herbelin	2002-12-04