coq - The formal proof system

Age	Commit message (Expand)	Author
2001-03-01	backtrack unification types et deplacement make_clenv_binding	filliatr
2001-03-01	nouvelle implantation de la reduction	barras
2001-02-28	introduction d'un refine avec resolution des types et de l'instantiation des ...	mohring
2001-02-28	modif	mohring
2001-02-28	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-27	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-26	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-22	Stringmap -> Idmap	herbelin
2001-02-22	extraction des types et des inductifs	filliatr
2001-02-21	nouveau design ou le renommage sera fait a posteriori	filliatr
2001-02-20	mise en place fichiers extraction	filliatr
2001-02-16	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-14	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-13	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-12	Bug nombres en chiffres décimaux dans les Cases	herbelin
2001-02-12	Theoreme opaques	mohring
2001-02-10	All errors were not well reported before. In particular syntax errors were	bertot