coq - The formal proof system

Age	Commit message (Expand)	Author
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
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-11	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-10	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-09	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-07	maj	filliatr
2004-02-07	maj	filliatr