coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	reorganize the order of librairies in the entry CMO to make sure this can	bertot	2004-02-02
*	adds the possibility to mark function arguments as formulas in Ltac	bertot	2004-02-02
*	adds the possibility to mark function arguments as formulas in Ltac	bertot	2004-02-02
*	maj	filliatr	2004-01-31
*	updates the definition of tactics using Ltac and adds the subst tactic	bertot	2004-01-30
*	adds module commands and update the extration command	bertot	2004-01-30
*	maj	filliatr	2004-01-30
*	maj	filliatr	2004-01-30
*	pour win32	coq	2004-01-29
*	Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...	herbelin	2004-01-29
*	Reparation d'une rupture (en presence de types implicites) de l'invariant que...	herbelin	2004-01-29
*	pour ide sous windows	coq	2004-01-29
*	MAJ	herbelin	2004-01-29
*	Suppression de 'Print.' en v8	herbelin	2004-01-29
*	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...	herbelin	2004-01-29
*	updates the tactics contradiction and autorewrite, the commands	bertot	2004-01-29
*	maj	filliatr	2004-01-29
*	Bug de Require multiple	herbelin	2004-01-28
*	make sure that 'in' clauses for reduction tactics are translated	bertot	2004-01-28
*	maj	filliatr	2004-01-28
*	maj	filliatr	2004-01-28