coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Localisation erreur interp_notation	herbelin	2004-02-12
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
*	Mauvaise dependance en states7/initial.coq	herbelin	2004-02-12
*	Localisation erreur interp_notation	herbelin	2004-02-12
*	Correction bug affichage en presence de '{ _ }'	herbelin	2004-02-12
*	lazy was translated to cbv, obviously wrong	bertot	2004-02-12
*	Ajout delimiteur pour bool_scope	herbelin	2004-02-12
*	MAJ	herbelin	2004-02-12
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
*	Implicits can have an optional list of argument, which is different	bertot	2004-02-12
*	maj	filliatr	2004-02-12
*	a new version that uses intro patterns, but the code still needs some cleaning	bertot	2004-02-11
*	removes a lot comments that may be useful for later code maintenance, but	bertot	2004-02-11
*	maj	filliatr	2004-02-11
*	Correction of a bug in Functional Scheme discovered when porting the	coq	2004-02-10
*	backtrack implicit dans Bvector	marche	2004-02-10
*	maj	filliatr	2004-02-10
*	New version of Functional Scheme and functional induction. Deals with	coq	2004-02-09
*	patch Bvector: args implicites	marche	2004-02-09
*	maj	filliatr	2004-02-09
*	maj	filliatr	2004-02-07
*	maj	filliatr	2004-02-07
*	MAJ	herbelin	2004-02-06
*	Test dependencies in constructors	herbelin	2004-02-06
*	correction de bugs de congruence et firstorder (inductifs)	corbinea	2004-02-06
*	Ajout filtrage sur motifs dépendants dans des inductifs différents	herbelin	2004-02-06
*	maj	filliatr	2004-02-06
*	On s'affranchit de l'information inductif ou pas dans le prédicat (càd	herbelin	2004-02-05
*	Suppression des types dans la signature du predicat (ils sont	herbelin	2004-02-05
*	maj	filliatr	2004-02-05
*	maj	filliatr	2004-02-05
*	Reconnaissance précoce de la dépendance du prédicat en un terme filtré	herbelin	2004-02-04
*	Vérification de la prise en compte des termes de type non inductif	herbelin	2004-02-04
*	clean-ide plus precis	herbelin	2004-02-04
*	Localisation un tout petit peu moins abstraite des erreurs de garde, mais res...	herbelin	2004-02-04
*	Boite autour des quote pour eviter un retour a la ligne apres le premier guil...	herbelin	2004-02-04
*	bug fix find coqide	coq	2004-02-04
*	highlight	marche	2004-02-04
*	search window	coq	2004-02-04
*	maj	filliatr	2004-02-04
*	MAJ	herbelin	2004-02-03
*	Relachement condition pour afficher @ en cas d'explicitation d'implicites	herbelin	2004-02-03
*	Relachement condition pour declarer un inductif dans la table des 'If'; contr...	herbelin	2004-02-03
*	Backtrack sur recuperation de noms a partir du type, car casse la correction ...	herbelin	2004-02-03
*	Bug focus	herbelin	2004-02-03
*	Protection contre noms de variable indefinis et guillemets autour des constr	herbelin	2004-02-03
*	Politique de filtrage pour l'affichage plus coercitif pour les lieurs : un no...	herbelin	2004-02-03
*	maj	filliatr	2004-02-03