coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	branchement extraction (bytecode seulement)	filliatr	2001-03-30
*	amelioration de la structure des univers	barras	2001-03-28
*	amelioration de la consommation memoire de la conversion en eta-expansant	barras	2001-03-23
*	Bug MUTCASE au lieu CASE	herbelin	2001-03-22
*	entetes	filliatr	2001-03-15
*	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin	2001-03-11
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	Bug affichage coercions	herbelin	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-16
*	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-14
*	Bug nommage Stdlib	herbelin	2001-02-13
*	Bug nombres en chiffres décimaux dans les Cases	herbelin	2001-02-12
*	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-09
*	modif de la syntax: assoc a droite pour Ring	mayero	2001-02-08
*	Simplifications	herbelin	2001-02-08
*	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-07
*	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-06
*	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-05
*	* empty log message *	mohring	2001-02-01
*	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-31
*	backtrack sur le lexeur de la V6	filliatr	2001-01-30
*	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-27
*	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-24
*	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-19
*	Meta Definition + Tactic Definition	delahaye	2001-01-09
*	Arite cachee de Match Context + Meta Definition	delahaye	2001-01-05
*	Ajout du Let pour le langage de tactiques	delahaye	2000-12-29
*	Pattern sera mieux dans Pretyping; relâchement head_pattern_bound	herbelin	2000-12-26