coq - The formal proof system

Age	Commit message (Expand)	Author
2001-09-21	Réparation des options Set Printing and co	herbelin
2001-09-20	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-19	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-14	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-10	Hack pour gérer les univers dans les prédicats de Cases synthétisés	herbelin
2001-09-09	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-07	Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)	herbelin
2001-09-04	erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies	barras
2001-08-13	bug de Bruijn	herbelin
2001-08-10	Parsing	herbelin
2001-07-24	Bug Simpl	herbelin
2001-07-21	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-06	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-05	Débogage discharge des coercions; nettoyage	herbelin
2001-07-04	message Ambiguous paths seulement si verbose	filliatr
2001-07-02	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin
2001-06-29	traitement du let dans red_product (tactique Red)	barras
2001-06-25	Bug dépendances non pertinentes (dû à des K-rédex) dans le type des branc...	herbelin
2001-06-20	Normalisation du predicat synthetise pour les Case	clrenard
2001-06-16	code mort	herbelin
2001-06-12	Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes aut...	clrenard
2001-05-29	Facilites pour le debogguage des univers.	coq
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-15	Modification pour passage p-automates	mohring
2001-05-15	Correction bug predicat du Cases (suite)	herbelin
2001-05-12	Bug propagation du predicat des Cases	herbelin
2001-05-10	Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)	herbelin
2001-05-03	Changement de la structure des points fixes	barras
2001-04-25	Bug perte d'alias avec type dependents	herbelin
2001-04-15	Bug affichage ordre des variables d'un pattern	herbelin
2001-04-13	Mise en place d'un test de clauses non utilisees	herbelin
2001-04-10	Bug context incoherent au passage du lambda et du let dans evar_eqappr	herbelin
2001-04-02	bug Fix signalé par Alexandre (even/odd mal interprété)	filliatr
2001-03-29	deux fois $Id$	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-23	amelioration de la consommation memoire de la conversion en eta-expansant	barras
2001-03-15	entetes	filliatr
2001-03-14	Alias suite + bugs divers et variés	herbelin
2001-03-14	Prise en compte des Let dans l'instance des evars	herbelin