coq - The formal proof system

Age	Commit message (Expand)	Author
2003-09-30	'_ = _ = _' maintenant predefini, meme en V7	herbelin
2003-09-30	Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'	herbelin
2003-09-30	Les notations hors scope s'empilent maintenant comme des scopes ne	herbelin
2003-09-30	code mort	herbelin
2003-09-30	Les notations hors scope s'empilent maintenant comme des scopes ne	herbelin
2003-09-30	Ajout 'Close Scope'.	herbelin
2003-09-30	Ajout 'Close Scope'.	herbelin
2003-09-30	Ajout 'Close Scope'.	herbelin
2003-09-29	Oubli du type du terme a filtrer quand pas d'argument dans la traduction de case	herbelin
2003-09-29	Prise en compte d'un inductif sans argument dans le 'in' des 'match'	herbelin
2003-09-28	oups	letouzey
2003-09-28	2 pbs de plus réglés concernant Setoid Ring:	letouzey
2003-09-28	une induction de moins dans lt_eq_lt_dec	letouzey
2003-09-28	well_founded_induction de nouveau transparent	letouzey
2003-09-27	maj	filliatr
2003-09-26	Bug about	herbelin
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