coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	traducteur: affiche les commentaires a l'interieur des commandes	barras	2003-09-22
*	L'exemple phare de modules - simplifie pour TPHOLs	coq	2003-09-22
*	MAJ	herbelin	2003-09-22
*	Anglais	herbelin	2003-09-22
*	Système de renommage des noms de tactiques Ltac	herbelin	2003-09-22
*	Bug d'externalisation des constantes avec uniquement des implicites	herbelin	2003-09-22
*	suite (et fin) reparation Setoid Ring	letouzey	2003-09-22
*	typo (Benjamin, voyons ;)	letouzey	2003-09-22
*	Distfix aussi adopte le nouveau schema de V8only	herbelin	2003-09-22
*	Implicits maintenant au courant pour l'affichage	herbelin	2003-09-22
*	Deplacement de lemmes de IntMap vers ZArith	herbelin	2003-09-22
*	tentative de rafraichissement de Setoid Ring	letouzey	2003-09-22
*	message d'erreur de garde des cofix	barras	2003-09-22
*	Passage à la V8 par défaut	herbelin	2003-09-22
*	Renommage Implicits -> Implicit	herbelin	2003-09-21
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
*	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
*	Changement de la politique de V8only: V8only tout seul signifie	herbelin	2003-09-21
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
*	Conflit de nom Pplus dans positive et dans polynomial (de ring)	herbelin	2003-09-21
*	Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...	herbelin	2003-09-21
*	Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...	herbelin	2003-09-21
*	Nettoyage	herbelin	2003-09-21
*	coqide auto complete initial bug fix	marche	2003-09-19
*	Coqide : les nouveaute d'aout	monate	2003-09-19
*	'::' est deja pris en V7	herbelin	2003-09-19
*	maj	filliatr	2003-09-19
*	Section et report Infix hors section	herbelin	2003-09-19
*	Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...	herbelin	2003-09-19
*	Mise en place des V8Notation et V8Infix pour déclarer des notations en	herbelin	2003-09-19
*	Ajout notation :: pour cons	herbelin	2003-09-19
*	Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...	herbelin	2003-09-19
*	parsing	herbelin	2003-09-19
*	Interface Eauto	herbelin	2003-09-18
*	Traduction de Instantiate	herbelin	2003-09-18
*	Niveau du 'as' des motifs	herbelin	2003-09-18
*	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