coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout d'un fichier license	mohring	2001-03-09
*	Mise a jour credits pour la V7	mohring	2001-03-09
*	corrections de bug de la reduction	barras	2001-03-08
*	compare_constr independent du groupement des applications.	barras	2001-03-08
*	changement comparaison etats	filliatr	2001-03-08
*	distinction contexte et signature	filliatr	2001-03-07
*	plus de commentaires	letouzey	2001-03-06
*	on gele apres un Require => meilleures performances memoire, en particulier p...	filliatr	2001-03-06
*	réparation (?) discharge axiome	filliatr	2001-03-06
*	Modification de e_give_exact pour eviter d'echouer sur l'unification	mohring	2001-03-06
*	eta-expansion	mohring	2001-03-06
*	EAutod (debug)	filliatr	2001-03-06
*	modifs pour extraction; bug coqmktop	filliatr	2001-03-06
*	ocamlweb	filliatr	2001-03-05
*	extraction termes (suite)	filliatr	2001-03-05
*	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr	2001-03-05
*	indentation code	filliatr	2001-03-05
*	Re-Déplacement extended_rel_list	herbelin	2001-03-05
*	Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ...	herbelin	2001-03-05
*	De bizarres SR_pus_assoc au lieu de SR_plus_assoc	herbelin	2001-03-01
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	Inversion termast/astterm; suppression camldebug pour coqmktop -opt	herbelin	2001-03-01
*	backtrack unification types et deplacement make_clenv_binding	filliatr	2001-03-01
*	nouvelle implantation de la reduction	barras	2001-03-01
*	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-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