coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Independance de grammar.cmo vis a vis de Search	herbelin	2003-10-23
*	Suppression dependance formelle en Vernacexpr	herbelin	2003-10-22
*	Integration de SearchNamed dans SearchAbout	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par...	herbelin	2003-10-21
*	Extension de Locate	herbelin	2003-10-21
*	On n'autorise plus les niveaux doubles L/R en v8	herbelin	2003-10-17
*	Bug mot-cle TYPES	herbelin	2003-10-17
*	Traduction des idents aussi dans le printer generique des tactiques	herbelin	2003-10-17
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	lettac -> set	barras	2003-10-16
*	Bug Search	herbelin	2003-10-16
*	Mise en conformite return_type en fonction de la doc	herbelin	2003-10-15
*	Changement 'as notation' en 'where notation'	herbelin	2003-10-14
*	Ameliration affichage inductifs	herbelin	2003-10-13
*	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin	2003-10-13
*	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin	2003-10-13
*	Ajout fnl() dans About	herbelin	2003-10-11
*	mise a jour nouvelle syntaxe	barras	2003-10-11
*	Suppression Grammar/Syntax	herbelin	2003-10-10
*	Delimiters N devient 'nat'	herbelin	2003-10-10
*	Cablage en dur de inversion	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Compatibilite ocaml 3.06 et 3.07	herbelin	2003-10-09
*	Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé in...	herbelin	2003-10-08
*	Essai de traduction du contraire de 'tacledit bin/coqtop.byte' en 'tac...'	herbelin	2003-10-07
*	Debranchement de l'affichage automatique de Proof par le traducteur (trop com...	herbelin	2003-10-07
*	Inspect saute maintenant les marqueurs invisibles	herbelin	2003-10-07
*	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