coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix d'un bug de Tauto	delahaye	2001-06-15
*	Prise en compte env local (et defs locales) dans Change	herbelin	2001-06-13
*	Correction d'un bug du a un Intros trop violent	delahaye	2001-06-01
*	Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ...	herbelin	2001-06-01
*	Amelioration - subjective - de l'affichage des Hint	herbelin	2001-05-31
*	Pretty -> Prettyp	filliatr	2001-05-28
*	Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types	herbelin	2001-05-25
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Changement de la structure des points fixes	barras	2001-05-03
*	Ajout du cas True->A\|-B	delahaye	2001-04-24
*	Fonction lookup enlevee	delahaye	2001-04-19
*	Mise en page	herbelin	2001-04-15
*	Ajout de _ dans les patterns d'intro	mohring	2001-04-12
*	Mis un message d'erreur explicite pour l'echec de Elim en cas	mohring	2001-04-12
*	Make it possible to perform proofs by induction even on non-inductive types,	bertot	2001-04-03
*	amelioration de la structure des univers	barras	2001-03-28
*	Problèmes de NewInduction	herbelin	2001-03-22
*	entetes	filliatr	2001-03-15
*	bug de refine: uncaught exception Array.sub	barras	2001-03-09
*	changement comparaison etats	filliatr	2001-03-08
*	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
*	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr	2001-03-05
*	Déplacement de qualid dans Nametab, hors du noyau	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
*	modif	mohring	2001-02-28
*	EAuto mixte (largeur puis profondeur)	mohring	2001-02-27
*	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
*	ident au lieu de string pour le nom de base de qualid	herbelin	2001-02-16
*	Prise en compte noms longs dans SuperAuto	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 affichage	herbelin	2001-02-14
*	Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...	herbelin	2001-02-14
*	code mort	herbelin	2001-02-07
*	EqDecide	filliatr	2001-02-06
*	Ajout d'une heuristique pour les types dependants	delahaye	2001-02-05
*	Message d'erreur plus explicite pour Tauto	delahaye	2001-02-05
*	rétablissement nouveau Tauto	filliatr	2001-02-05
*	Résolution d'un bug de simplification	delahaye	2001-02-03
*	application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés	filliatr	2001-02-01
*	oubli de Closure.EvalConstRef	filliatr	2001-02-01
*	- coqc : option -image	filliatr	2001-02-01
*	Mise en place de la possibilite d'unfolder des variables locales et des const...	filliatr	2001-01-31
*	Bug fixed: the case [ id : ?1 -> ?2 \|- ?] was missing in tauto_main	sacerdot	2001-01-30
*	As an heuristic, now both in tauto and intuition we try to avoid the initial	sacerdot	2001-01-29