coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	retire profile	mohring	2001-02-28
*	Changement de subst_meta	mohring	2001-02-28
*	Typo message Scheme	herbelin	2001-02-28
*	bug Reset et Sections	filliatr	2001-02-28
*	debut extraction termes; pp lambda	filliatr	2001-02-27
*	Ajout d'un test sur EAuto	mohring	2001-02-27
*	EAuto mixte (largeur puis profondeur)	mohring	2001-02-27
*	ajout Vprop, Tprop et Eprop	filliatr	2001-02-26
*	changement message d'erreur Abstract	filliatr	2001-02-26
*	Eauto version en largeur	mohring	2001-02-26
*	Abstract: on échoue si le but contient des existentielles	filliatr	2001-02-26
*	mise a jour	filliatr	2001-02-26
*	export open_trapping_failure pour contrib/extraction	filliatr	2001-02-26
*	Stringmap -> Idmap	herbelin	2001-02-22
*	extraction des types et des inductifs	filliatr	2001-02-22
*	nouveau design ou le renommage sera fait a posteriori	filliatr	2001-02-21
*	mise en place fichiers extraction	filliatr	2001-02-20
*	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
*	MAJ	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
*	Erreur sur commit	herbelin	2001-02-14
*	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin	2001-02-14
*	Renommage des variables dans les schémas d'induction	herbelin	2001-02-14
*	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin	2001-02-14
*	Bug affichage	herbelin	2001-02-14
*	MAJ	herbelin	2001-02-14
*	mise a jour	filliatr	2001-02-14
*	Stdlib -> Coqlib, Stock disparait	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-14
*	prise en compte des défs locales dans les arguments des inductifs; meilleure...	herbelin	2001-02-14
*	Restructuration	herbelin	2001-02-14
*	uniformisation avec constr des lieurs dans rawterm/pattern	herbelin	2001-02-14
*	Obsolète (cf Coqlib)	herbelin	2001-02-14
*	Test syntaxe avec motifs numériques	herbelin	2001-02-14
*	Absolute URL for DTDs introduced	sacerdot	2001-02-13
*	Bug nommage Stdlib	herbelin	2001-02-13
*	export a function that is needed in pcoq.	bertot	2001-02-13
*	Make sure the initial state used in a protected loop is the state chose exactly	bertot	2001-02-13
*	Bug nombres en chiffres décimaux dans les Cases	herbelin	2001-02-12
*	Theoreme opaques	mohring	2001-02-12
*	All errors were not well reported before. In particular syntax errors were	bertot	2001-02-10
*	Two pairs of parentheses were missing.	bertot	2001-02-09
*	option -m (utilisation memoire)	filliatr	2001-02-09
*	Bug point final dans la syntaxe theorem_body	herbelin	2001-02-09
*	MAJ	herbelin	2001-02-09