coq - The formal proof system

Age	Commit message (Expand)	Author
2004-02-21	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-20	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-19	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-18	- 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-17	Ajout de lconstr, constr et binder_constr dans Print Grammar constr	herbelin
2004-02-17	maj	filliatr
2004-02-17	maj	filliatr
2004-02-16	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-14	maj	filliatr
2004-02-14	maj	filliatr
2004-02-13	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-12	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	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