coq - The formal proof system

Age	Commit message (Expand)	Author
2004-03-01	maj	filliatr
2004-02-28	Exemple de Frederic	herbelin
2004-02-28	Expansion du type par nécessité dans le cas d'affichage d'implicites	herbelin
2004-02-28	MAJ Commentaires	herbelin
2004-02-28	Traduction 'Cases' en pattern-matching	herbelin
2004-02-28	Eviter la stricte redondance de regles de grammaires v7	herbelin
2004-02-28	Prise en compte des implicites au travers des notations et abbreviations	herbelin
2004-02-28	maj	filliatr
2004-02-27	MAJ	herbelin
2004-02-27	Erreur de Bruijn et oubli substitution alias dans annotation du 'match'	herbelin
2004-02-27	Ajout test synthese du predicat a partir du cast d'un filtrage avec dependances	herbelin
2004-02-27	* empty log message *	filliatr
2004-02-27	maj	filliatr
2004-02-26	added breakpoints to help ide	corbinea
2004-02-26	Keep structure information for Fixpoint declaration and Fix terms	bertot
2004-02-26	Not all cases for coercions and locality were handled	bertot
2004-02-26	Inclusion des annotations de type des filtrages dans 'Set Printing All'	herbelin
2004-02-26	maj	filliatr
2004-02-25	indexation Record / bug gallina sur := en V8	filliatr
2004-02-25	maj	filliatr
2004-02-25	maj	filliatr
2004-02-24	coqdoc	filliatr
2004-02-24	* empty log message *	filliatr
2004-02-24	coqdoc	filliatr
2004-02-24	maj	filliatr
2004-02-23	Generating of annotations added to Makefile.dir	coq
2004-02-23	corrects the treatement of SubClass declarations	bertot
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