coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	coqdoc	filliatr	2004-02-24
*	* empty log message *	filliatr	2004-02-24
*	coqdoc	filliatr	2004-02-24
*	maj	filliatr	2004-02-24
*	Generating of annotations added to Makefile.dir	coq	2004-02-23
*	corrects the treatement of SubClass declarations	bertot	2004-02-23
*	Correction oubli de report d'une modification de g_vernac (1.69) vers g_verna...	herbelin	2004-02-21
*	MAJ	herbelin	2004-02-21
*	Export des arguments scope au chargement, pas a l'ouverture (2eme)	herbelin	2004-02-21
*	maj	filliatr	2004-02-21
*	Export des arguments scope au chargement, pas a l'ouverture	herbelin	2004-02-20
*	commit précédent erroné	herbelin	2004-02-20
*	maj	filliatr	2004-02-20
*	maj	filliatr	2004-02-20
*	makes sure the following examples are well-treated:	bertot	2004-02-19
*	files from contrib/interface need files from contrib/field, the variable	bertot	2004-02-19
*	Bugs/insuffisances trouvees en traduisant MMode	herbelin	2004-02-19
*	maj	filliatr	2004-02-19
*	maj	filliatr	2004-02-19
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	Bug coercions imbriquees + suppression des coercions avant filtrage sur notat...	herbelin	2004-02-18
*	maj	filliatr	2004-02-18
*	Ajout de lconstr, constr et binder_constr dans Print Grammar constr	herbelin	2004-02-17
*	maj	filliatr	2004-02-17
*	maj	filliatr	2004-02-17
*	Erreur dépendance en Util lui-même	herbelin	2004-02-16
*	accomodate the .. extension	bertot	2004-02-16
*	adds a new command for searching a pattern inside the premises of theorems	bertot	2004-02-16
*	corrects a bug in name reservation, simplifies or_intro, removes dead code	bertot	2004-02-16
*	export the general function for getting information from the environment	bertot	2004-02-16
*	maj	filliatr	2004-02-16
*	maj	filliatr	2004-02-14
*	maj	filliatr	2004-02-14
*	Deplacement array_map_left and co dans Util	herbelin	2004-02-13
*	Ajout array_map_left and co	herbelin	2004-02-13
*	Uniformisation du comportement de Notation et Reserved Notation	herbelin	2004-02-13
*	Correction d'un pb '{ _ }' et uniformisation du comportement de Notation et R...	herbelin	2004-02-13
*	petit bug avec Extraction Optimize	letouzey	2004-02-13
*	Bug numerotation des occurrences pour 'simpl id at n' (suite)	herbelin	2004-02-13
*	adds a new command add_rec_path for the parser program and changes add_path	bertot	2004-02-13
*	Bug numerotation des occurrences pour 'simpl id at n' (2 protections maintena...	herbelin	2004-02-13
*	adds the possibility to have terms (and not just identifiers) as hints	bertot	2004-02-13
*	adds the possibility to have terms (and not just identifiers) as hints	bertot	2004-02-13
*	maj	filliatr	2004-02-13
*	maj	filliatr	2004-02-13
*	Typo	herbelin	2004-02-12
*	Plus d'explicitation d'un message d'erreur	herbelin	2004-02-12
*	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