coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Plus de nom commencant par '_' en V8	herbelin	2003-10-02
*	Le nom '_' n'est plus valable en v8 pour nommer les variables	herbelin	2003-10-02
*	Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...	herbelin	2003-10-01
*	cosmetique	herbelin	2003-10-01
*	Implantation de l'option 'format' des Notations	herbelin	2003-10-01
*	maj	filliatr	2003-10-01
*	'_ = _ = _' 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-30
*	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-29
*	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-28
*	maj	filliatr	2003-09-27
*	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-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