coq - The formal proof system

Age	Commit message (Expand)	Author
2003-04-26	bugfix in Ground tactic	corbinea
2003-04-26	maj	filliatr
2003-04-25	Added the Ground tactic.	corbinea
2003-04-25	utf8.v	monate
2003-04-25	new utf8.v	monate
2003-04-25	extension des caracteres UTF 8 autorises dans les symboles	filliatr
2003-04-24	* empty log message *	monate
2003-04-24	coqide : line number mode	monate
2003-04-24	* empty log message *	monate
2003-04-22	Coqide : bug undo	monate
2003-04-22	coqide : progressbar	monate
2003-04-18	maj	filliatr
2003-04-17	Intégration DatatypesSyntax à Datatypes	herbelin
2003-04-17	MAJ	herbelin
2003-04-17	Divers	herbelin
2003-04-17	<> maintenant standard	herbelin
2003-04-17	Intégration DatatypesSyntax à Datatypes	herbelin
2003-04-17	Syntaxe 'x=y:>T'	herbelin
2003-04-17	Ajout "at next level" dans Notation	herbelin
2003-04-17	commentaires	herbelin
2003-04-17	Ooops	letouzey
2003-04-17	maj	filliatr
2003-04-17	temporaire	letouzey
2003-04-16	BIG MAJ Extraction:	letouzey
2003-04-16	suite au commit d'hugo dans TypeSyntax & Raxiom, Intro donnait un nom different	letouzey
2003-04-16	oubli	letouzey
2003-04-16	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey
2003-04-16	une fonction list_skipn qui zappe les n premiers elements d'une liste	letouzey
2003-04-16	coupage en deux du bloc pas si mutuellement recursif des module_body & co (.....	letouzey
2003-04-16	prettyprint des constr_substituted + un wrapping de prglobal pour qu'il n'ech...	letouzey
2003-04-16	sumboolT, sumorT, sigTT, SigT redondants	herbelin
2003-04-16	On force l'affichage des implicites non '?' lors de la traduction	herbelin
2003-04-15	Débranchement des tests output qui sont faussés par le traducteur	herbelin
2003-04-15	Affichage coercions en mode -(f)translate	herbelin
2003-04-14	Cosmetique	herbelin
2003-04-14	Localisation des appels de tactiques définies sans arguments	herbelin
2003-04-14	Bug: lookup inapproprie dans subst_tactic	herbelin
2003-04-14	Correction bug PR#278	coq
2003-04-14	Local 'o'	herbelin
2003-04-12	Open Scope en Local	herbelin
2003-04-11	Ajout option 'Local' à Infix et Notation	herbelin
2003-04-11	Ajout option 'Local' à Infix et Notation	herbelin
2003-04-11	Explicitation arguments de eq	herbelin
2003-04-10	Affichage des inductifs	herbelin
2003-04-10	Open Scope remplace Import	herbelin
2003-04-10	Calcul automatique de l'implicite de nil pour que l'affichage sache le traiter	herbelin
2003-04-10	Affichage forcé des implicites contextuels si pas de contexte connu	herbelin
2003-04-10	Remplacement Import par Open Scope en v8	herbelin
2003-04-10	Suppression de quelques espaces superflus	herbelin
2003-04-10	Relachement globalisation Unfold en usage interactif	herbelin