coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-17
*	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-16
*	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-15
*	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-14
*	Open Scope en Local	herbelin	2003-04-12
*	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-11
*	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-10
*	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