coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Remplacement de Induction/Destruct par NewInduction/NewDestruct	herbelin	2003-09-23
*	Correction bug NewInduction pour les inductifs de type 'ordinaux'	herbelin	2003-09-23
*	Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...	herbelin	2003-09-23
*	Fonctions utiles	herbelin	2003-09-23
*	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
*	Ajout fonctions syntaxe v8 pour contrib MapleMode	herbelin	2003-09-23
*	Correction bug 328	coq	2003-09-23
*	test d'implicite incorrect depuis que eq porte sur Type	barras	2003-09-23
*	Bug internalisation des Extern: la globalisation doit etre stricte	herbelin	2003-09-23
*	maj	filliatr	2003-09-23
*	commit accidentel d'une bidouille	letouzey	2003-09-22
*	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