coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Induction -> NewInduction; '++' pour app	herbelin	2003-09-26
*	Nouvelle serie de traductions	herbelin	2003-09-26
*	Re-possibilite changement chaine infixe en passant v7 a v8	herbelin	2003-09-26
*	Passage de Destruct a NewDestruct; '-' pour negb	herbelin	2003-09-26
*	Structuration de fast_integer en operations sur positive, proprietes des oper...	herbelin	2003-09-26
*	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin	2003-09-26
*	Decouplage printing en v8 pour les interpretations de notations	herbelin	2003-09-26
*	Logic_TypeSyntax a disparu	herbelin	2003-09-25
*	add_x_x de fast_integer vers auxiliary	herbelin	2003-09-25
*	Retour provisoire a une section	herbelin	2003-09-25
*	V8Infix declarait a tort une regle d'interpretation V7	herbelin	2003-09-25
*	Passage options via COQFLAGS plutot que OPT	herbelin	2003-09-24
*	Traduction aussi si -translate et -load-vernac-source	herbelin	2003-09-24
*	Suppression section, ce qui evite de repliquer les declarations d'Infix	herbelin	2003-09-24
*	Destruct/Induction -> NewDestruct/NewInduction	herbelin	2003-09-24
*	Destruct -> NewDestruct	herbelin	2003-09-24
*	Utilisation de noms dans 'Implicit Arguments [...]'	herbelin	2003-09-24
*	maj	filliatr	2003-09-24
*	Remplacement de Induction/Destruct par NewInduction/NewDestruct	herbelin	2003-09-23
*	Remplacement de Induction/Destruct par NewInduction/NewDestruct	herbelin	2003-09-23
*	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