coq - The formal proof system

Age	Commit message (Expand)	Author
2001-02-16	ident au lieu de string pour le nom de base de qualid	herbelin
2001-02-16	Tentative d'amélioration affichage decls locales	herbelin
2001-02-16	Suppression sp_of_id	herbelin
2001-02-16	Prise en compte noms longs dans SuperAuto	herbelin
2001-02-16	Prise en compte noms longs dans Implicits	herbelin
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2001-02-14	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin
2001-02-13	Bug nommage Stdlib	herbelin
2001-02-12	Bug nombres en chiffres décimaux dans les Cases	herbelin
2001-02-09	Bug point final dans la syntaxe theorem_body	herbelin
2001-02-09	exported a few functions that are used in graphical interface pcoq.	bertot
2001-02-09	Several pairs of different functions actually had the same name, so	bertot
2001-02-08	modif de la syntax: assoc a droite pour Ring	mayero
2001-02-08	Simplifications	herbelin
2001-02-07	Modif pour les patterns de sous-termes	delahaye
2001-02-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2001-02-07	Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref	herbelin
2001-02-06	Ajout d'une commande pour afficher chaque coercion à la demande	herbelin
2001-02-06	Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...	herbelin
2001-02-05	Extension coerce_to_var	herbelin
2001-02-05	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin
2001-02-05	Restructuration de classops; évolution en une version mieux intégrée au re...	herbelin
2001-02-05	Correction pour Time pour ne pas etre oblige de mettre deux points	delahaye
2001-02-01	* empty log message *	mohring
2001-01-31	Bug localisation des Syntactif Definition	herbelin
2001-01-31	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr
2001-01-31	Ajout option Set/Unset/Test Printing Coercions	herbelin
2001-01-30	backtrack sur le lexeur de la V6	filliatr
2001-01-27	Simplification Impargs	herbelin
2001-01-27	Factorisation du '.' final	herbelin
2001-01-27	Ré-introduction des implicites à la volée dans la définition des inductifs	herbelin
2001-01-24	Prise en compte des noms longs dans les Hints et les Coercions	herbelin
2001-01-24	Ajout de constantes locales dans les Records	herbelin
2001-01-19	Prise en compte de constructeurs qualifiés dans les patterns	herbelin
2001-01-19	Nouveau module pour centraliser les chemins des constantes globales utilisée...	herbelin
2001-01-19	Ajout d'un parseur d'entiers sous forme de pattern	herbelin
2001-01-19	Autour des quotations avec Cases	herbelin
2001-01-19	Réparation bug extensibilité de Constr.pattern	herbelin
2001-01-09	Meta Definition + Tactic Definition	delahaye
2001-01-05	Arite cachee de Match Context + Meta Definition	delahaye
2000-12-29	Ajout du Let pour le langage de tactiques	delahaye
2000-12-26	Pattern sera mieux dans Pretyping; relâchement head_pattern_bound	herbelin
2000-12-25	bug head_pattern_bound	herbelin
2000-12-25	Token n'est plus un keyword	herbelin
2000-12-25	Effet réorganisation Classops	herbelin
2000-12-22	* empty log message *	mayero
2000-12-21	Qualification des inductifs dans Print ind	herbelin
2000-12-20	espacements	herbelin
2000-12-20	Suppression warning variable de filtrage en majuscule	herbelin
2000-12-20	ajout ident_or_constrarg pour NewInduction	herbelin