coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Hypothesis mot-cle	herbelin	2003-10-02
*	Implantation de l'option 'format' des Notations	herbelin	2003-10-01
*	Les notations hors scope s'empilent maintenant comme des scopes ne	herbelin	2003-09-30
*	Ajout 'Close Scope'.	herbelin	2003-09-30
*	Bug about	herbelin	2003-09-26
*	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'	herbelin	2003-09-26
*	Ajout 'About'	herbelin	2003-09-26
*	Re-possibilite changement chaine infixe en passant v7 a v8	herbelin	2003-09-26
*	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin	2003-09-24
*	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin	2003-09-23
*	Changement de l'afficheur pour que les variables liées aient un nom indépen...	herbelin	2003-09-23
*	traducteur: affiche les commentaires a l'interieur des commandes	barras	2003-09-22
*	Distfix aussi adopte le nouveau schema de V8only	herbelin	2003-09-22
*	Renommages divers.	herbelin	2003-09-21
*	Changement de la politique de V8only: V8only tout seul signifie	herbelin	2003-09-21
*	Parsing au niveau lconstr des patterns de 'match context'	herbelin	2003-09-21
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
*	Mise en place des V8Notation et V8Infix pour déclarer des notations en	herbelin	2003-09-19
*	Ajout r gle d'affichage tactiques èéfinies par Notation	herbelin	2003-09-18
*	Simplification afficheur de tactiques non primitive	herbelin	2003-09-18
*	En attendant l'afficheur...	herbelin	2003-09-16
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin	2003-09-12
*	Fusion des g_syntaxnew.ml avec les g_syntax.ml avec sélection dynamique selon	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 'Print Scopes' et 'Bind Scope with classes'; 'Delimits' -> 'Delimit'	herbelin	2003-09-12
*	Passage des projections au niveau 1	herbelin	2003-09-10
*	9 est associatif a gauche	herbelin	2003-09-10
*	Traduction de Distfix	herbelin	2003-09-10
*	Ajout construction If primitive dans constr_expr et rawconstr	herbelin	2003-09-09
*	'Grammar tactic' devient 'Tactic Notation'	herbelin	2003-09-09
*	Traduction des réferences arguments de commandes non primitives	herbelin	2003-09-09
*	Code mort	herbelin	2003-09-09
*	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin	2003-09-06
*	Mise en place possibilité de définitions locales dans les paramètres des r...	herbelin	2003-09-06
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
*	'Implicits qid' -> 'Implicit Arguments qid'	herbelin	2003-09-06
*	Adapter l'entree de grammaire a la version 7 ou 8	herbelin	2003-09-06
*	Mise en place possibilité de définitions locales dans les paramètres des i...	herbelin	2003-09-06
*	Passage de lconstr à constr pour les arguments immédiat de commandes	herbelin	2003-09-06
*	Passage de lconstr à constr pour les arguments immédiat de commandes	herbelin	2003-09-06
*	Bug affichage tactiques supplementaires en v8 (suite)	herbelin	2003-09-06
*	Bug affichage tactiques supplementaires en v8	herbelin	2003-09-05
*	Impression sans ',' des constructeurs de meme type, pour v8	herbelin	2003-09-05
*	Relachement conflit 'with' dans le cas des Module with Definition	herbelin	2003-09-02
*	'Assumptions' sur le modèle général des lieurs	herbelin	2003-08-31
*	Affichage des inductifs en v8	herbelin	2003-08-31
*	Pb de mot-cle	herbelin	2003-08-14
*	Ajout token '!' pour correctness	herbelin	2003-08-14