coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Traduction de '_' comme reference	herbelin	2003-09-18
*	Parsing correct des explicites en cas de projection	herbelin	2003-09-18
*	Plutôt que de faire "Load" silencieusement, en profiter pour traduire	herbelin	2003-09-18
*	Ajout r gle d'affichage tactiques èéfinies par Notation	herbelin	2003-09-18
*	Simplification afficheur de tactiques non primitive	herbelin	2003-09-18
*	bug fix: term reduced in bad env	barras	2003-09-18
*	maj	filliatr	2003-09-17
*	En attendant l'afficheur...	herbelin	2003-09-16
*	Pour appliquer les noms reserves aussi aux binders	herbelin	2003-09-16
*	Pour cacher le contenu de Load au traducteur	herbelin	2003-09-16
*	Tentative amelioration pretty-printing symboles	herbelin	2003-09-16
*	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)...	herbelin	2003-09-16
*	(Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)	herbelin	2003-09-16
*	Reprise de coqbinaries dans translation	herbelin	2003-09-15
*	Bug PR#324	herbelin	2003-09-14
*	Indirection pour coqlib8 pour que la cible newtheories/%.v soit choisie	herbelin	2003-09-13
*	Deplacement de Declare vers Termops	herbelin	2003-09-13
*	maj	filliatr	2003-09-13
*	Retour à des cibles plus explicites: world7 et world8, install7 et install8	herbelin	2003-09-12
*	Outil de test de la traduction et de la compilation en v8 sans modification des	herbelin	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