coq - The formal proof system

Age	Commit message (Expand)	Author
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
2003-04-10	coqide: undo fix	monate
2003-04-10	* empty log message *	monate
2003-04-10	* empty log message *	monate
2003-04-10	coqide: bug highlight corrige	monate
2003-04-10	coqide: completion support	monate
2003-04-10	set_focus	marche
2003-04-10	coqide: thread bug fix	monate
2003-04-10	Trop de restriction pour les TacDef	herbelin
2003-04-10	maj	filliatr
2003-04-09	cast de nil	herbelin
2003-04-09	Affichage des inductifs	herbelin
2003-04-09	nil en implicite dans la v8	herbelin
2003-04-09	Bug init_function	herbelin
2003-04-09	Synchronisation séparée des implicites pour l'affichage du traducteur;	herbelin
2003-04-09	Formattage affichage	herbelin
2003-04-09	Correction Show Implicits	herbelin
2003-04-09	Ajout Open Scope	herbelin
2003-04-09	Mécanisme plus simple et efficace pour traduire les implicites	herbelin