coq - The formal proof system

Age	Commit message (Expand)	Author
2003-09-12	Ajout install7 et coqwc dans tools	herbelin
2003-09-12	Ajout cible world7	herbelin
2003-09-12	Divers	herbelin
2003-09-12	Ajout nouvelles commandes	herbelin
2003-09-12	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin
2003-09-12	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin
2003-09-12	Suppression DatatypesSyntax et PeanoSyntax qui était vides	herbelin
2003-09-12	Fusion des g_syntaxnew.ml avec les g_syntax.ml avec sélection dynamique selon	herbelin
2003-09-12	Inclusion automatique de highparsing	herbelin
2003-09-12	Suppression DatatypesSyntax et PeanoSyntax qui était vides	herbelin
2003-09-12	Message pour les erreurs	herbelin
2003-09-12	Passage au numéro de version V8	herbelin
2003-09-12	MAJ	herbelin
2003-09-12	Indépendance vis à vis de Declare	herbelin
2003-09-12	Ajout 'Print Scopes' et 'Bind Scope with classes'	herbelin
2003-09-12	MAJ module requis pour le parsing des numéraux	herbelin
2003-09-12	Affichage des scopes d'arguments	herbelin
2003-09-12	Ajout et MAJ commandes de scopes	herbelin
2003-09-12	Activation déclaration automatique de scope d'arguments; affichage scopes d'...	herbelin
2003-09-12	Bind et Delimit pour R	herbelin
2003-09-12	Indépendance vis à vis de Declare	herbelin
2003-09-12	Déplacement d'un morceau de Declare	herbelin
2003-09-12	Bind et Delimit pour nat	herbelin
2003-09-12	Ajout 'Print Scopes' et 'Bind Scope with classes'	herbelin
2003-09-12	Bind et Delimit pour positive et Z (hors section)	herbelin
2003-09-12	Bind et Delimit pour R	herbelin
2003-09-12	Déplacement de Declare et Impargs à la fin de interp pour que Declare accè...	herbelin
2003-09-12	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin
2003-09-12	Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...	herbelin
2003-09-12	Activation déclaration automatique de scope d'arguments	herbelin
2003-09-12	Déplacement de Declare et déclarations des scopes d'argument dans Declare	herbelin
2003-09-12	Mise en place affichage spécifique pour le scope des types	herbelin
2003-09-12	Scope type pour le codomaine de Prod aussi; ajout extern_rawtype	herbelin
2003-09-12	Scope type pour le codomaine de Prod aussi	herbelin
2003-09-12	Ajout 'Print Scopes' et 'Bind Scope with classes'; 'Delimits' -> 'Delimit'	herbelin
2003-09-12	Ajout 'Print Scopes' et 'Bind Scope with classes'; Mise en place affichage sp...	herbelin
2003-09-12	open superflu	herbelin
2003-09-12	Simplification vis a vis de Declare	herbelin
2003-09-12	Branchement constant sur Coqlib	herbelin
2003-09-11	Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...	herbelin
2003-09-11	Nettoyage	herbelin
2003-09-11	maj	filliatr
2003-09-10	Renommage des variables '_'	herbelin
2003-09-10	Passage des projections au niveau 1	herbelin
2003-09-10	9 est associatif a gauche	herbelin
2003-09-10	Debranchement du traducteur pour Load !	herbelin
2003-09-10	warning vers std_err	herbelin
2003-09-10	Bug predicat old Case	herbelin
2003-09-10	Traduction de Distfix	herbelin
2003-09-10	typo	narboux