coq - The formal proof system

Age	Commit message (Expand)	Author
2003-09-26	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'	herbelin
2003-09-26	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'; trad...	herbelin
2003-09-26	MAJ	herbelin
2003-09-26	pa_ifdef.cmo redondant	herbelin
2003-09-26	Ajout now_show	herbelin
2003-09-26	About, Infix	herbelin
2003-09-26	'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...	herbelin
2003-09-26	Ajout 'About'	herbelin
2003-09-26	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-25	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-24	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-23	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-22	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