coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Réparation des options Set Printing and co	herbelin	2001-09-21
*	Transparent	barras	2001-09-20
*	Le prédicat du vieux Case ne doit pas contenir d'univers algébrique même q...	herbelin	2001-09-20
*	Blindage, de peur que des types entrant non en forme normale ne provoque des ...	herbelin	2001-09-19
*	Nouvelle fonction get_sort_family_of pour calculer la famille dans lequel vit...	herbelin	2001-09-19
*	Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...	herbelin	2001-09-19
*	Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ...	herbelin	2001-09-19
*	Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)	herbelin	2001-09-14
*	L'instantiation des evars quand un produit ou une sorte étaient attendus n'�...	herbelin	2001-09-14
*	L'instantiation des evars quand un produit ou une sorte étaient attendus n'�...	herbelin	2001-09-14
*	Hack pour gérer les univers dans les prédicats de Cases synthétisés	herbelin	2001-09-10
*	Nettoyage reduce_to_ind et one_step_reduce	herbelin	2001-09-09
*	Passage aux univers algébriques	herbelin	2001-09-09
*	Préparation du prétypage à la mise en place d'univers algébriques	herbelin	2001-09-09
*	Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)	herbelin	2001-09-07
*	erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies	barras	2001-09-04
*	bug de Bruijn	herbelin	2001-08-13
*	Parsing	herbelin	2001-08-10
*	Bug Simpl	herbelin	2001-07-24
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin	2001-07-21
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin	2001-07-21
*	Les tables de coercions ne doivent pas survivre aux sections	herbelin	2001-07-06
*	la conversion ne doit être testé dans evar_conv qu'en absence de evar	herbelin	2001-07-06
*	has_undefined_isevars était buggé	herbelin	2001-07-06
*	Débogage discharge des coercions; nettoyage	herbelin	2001-07-05
*	message Ambiguous paths seulement si verbose	filliatr	2001-07-04
*	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin	2001-07-02
*	traitement du let dans red_product (tactique Red)	barras	2001-06-29
*	Bug dépendances non pertinentes (dû à des K-rédex) dans le type des branc...	herbelin	2001-06-25
*	Normalisation du predicat synthetise pour les Case	clrenard	2001-06-20
*	code mort	herbelin	2001-06-16
*	Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes aut...	clrenard	2001-06-12
*	Facilites pour le debogguage des univers.	coq	2001-05-29
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
*	Modification pour passage p-automates	mohring	2001-05-15
*	Correction bug predicat du Cases (suite)	herbelin	2001-05-15
*	Bug propagation du predicat des Cases	herbelin	2001-05-12
*	Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)	herbelin	2001-05-10
*	Changement de la structure des points fixes	barras	2001-05-03
*	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