coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bug perte d'alias avec type dependents	herbelin	2001-04-25
*	Bug affichage ordre des variables d'un pattern	herbelin	2001-04-15
*	Mise en place d'un test de clauses non utilisees	herbelin	2001-04-13
*	Bug context incoherent au passage du lambda et du let dans evar_eqappr	herbelin	2001-04-10
*	bug Fix signalé par Alexandre (even/odd mal interprété)	filliatr	2001-04-02
*	deux fois $Id$	filliatr	2001-03-29
*	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
*	entetes	filliatr	2001-03-15
*	Alias suite + bugs divers et variés	herbelin	2001-03-14
*	Prise en compte des Let dans l'instance des evars	herbelin	2001-03-14
*	Rien au lieu erreur si plusieurs cas par défaut; quasi-achèvement alias dé...	herbelin	2001-03-12
*	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin	2001-03-11
*	Avancée vers la prise compte des alias dépendants; prise en compte des clau...	herbelin	2001-03-11
*	Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation	herbelin	2001-03-11
*	Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ...	herbelin	2001-03-05
*	Déplacement de qualid dans Nametab, hors du noyau	herbelin	2001-03-01
*	nouvelle implantation de la reduction	barras	2001-03-01
*	uniformisation avec constr des lieurs dans rawterm/pattern	herbelin	2001-02-14
*	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 demandeparsing/g_bas...	herbelin	2001-02-06
*	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
*	Reparation reduce_to_mind	mohring	2001-02-01
*	- coqc : option -image	filliatr	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
*	Prise en compte du let-in dans lookup_*_as_renamed	herbelin	2001-01-30
*	Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...	herbelin	2001-01-24
*	Nouveaux bugs instanciation d'evar par des evar	herbelin	2001-01-19
*	Bug environnement	herbelin	2001-01-11
*	Rajout de la restriction de l'instance en cas d'unification de 2 variables ex...	herbelin	2001-01-04
*	Rattrapage d'erreur pour le Case + Eval Compute in pour Definition	delahaye	2001-01-03
*	Bug de contextes	herbelin	2000-12-26
*	Déplacement du type stack de Reduction vers Closure et utilisation pour acc�...	herbelin	2000-12-26
*	Pattern sera mieux dans Pretyping; relâchement head_pattern_bound	herbelin	2000-12-26
*	Un nom long pour les variables de section qui font classe ou coercion; réorg...	herbelin	2000-12-25
*	Bug vieux Match	herbelin	2000-12-25
*	Bug prédicat	herbelin	2000-12-25
*	Bug prédicat old Case/Match	herbelin	2000-12-20
*	Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...	herbelin	2000-12-20
*	Export fonction testant si un inductive est un record	herbelin	2000-12-19
*	Amélioration message d'erreur mauvais prédicat	herbelin	2000-12-18
*	Debut de nettoyage de Simpl	mohring	2000-12-18
*	Suppression du warning several default clauses	herbelin	2000-12-16
*	Bug env vis à vis du let in	herbelin	2000-12-15
*	Bugs calcul du prédicat des Cases et Case	herbelin	2000-12-15
*	Printer	mohring	2000-12-15
*	Mauvais env donné à new_isevar	herbelin	2000-12-14
*	Oubli test de correction à l'instantiation des evars	herbelin	2000-12-14