aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2001-06-29traitement du let dans red_product (tactique Red)barras
2001-06-25Bug dépendances non pertinentes (dû à des K-rédex) dans le type des branc...herbelin
2001-06-20Normalisation du predicat synthetise pour les Caseclrenard
2001-06-16code mortherbelin
2001-06-12Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes aut...clrenard
2001-05-29Facilites pour le debogguage des univers.coq
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-15Modification pour passage p-automatesmohring
2001-05-15Correction bug predicat du Cases (suite)herbelin
2001-05-12Bug propagation du predicat des Casesherbelin
2001-05-10Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)herbelin
2001-05-03Changement de la structure des points fixesbarras
2001-04-25Bug perte d'alias avec type dependentsherbelin
2001-04-15Bug affichage ordre des variables d'un patternherbelin
2001-04-13Mise en place d'un test de clauses non utiliseesherbelin
2001-04-10Bug context incoherent au passage du lambda et du let dans evar_eqapprherbelin
2001-04-02bug Fix signalé par Alexandre (even/odd mal interprété)filliatr
2001-03-29deux fois $Id$filliatr
2001-03-28amelioration de la structure des universbarras
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
2001-03-15entetesfilliatr
2001-03-14Alias suite + bugs divers et variésherbelin
2001-03-14Prise en compte des Let dans l'instance des evarsherbelin
2001-03-12Rien au lieu erreur si plusieurs cas par défaut; quasi-achèvement alias dé...herbelin
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
2001-03-11Avancée vers la prise compte des alias dépendants; prise en compte des clau...herbelin
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
2001-03-05Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ...herbelin
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-03-01nouvelle implantation de la reductionbarras
2001-02-14uniformisation avec constr des lieurs dans rawterm/patternherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-02-06Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...herbelin
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au re...herbelin
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au re...herbelin
2001-02-01Reparation reduce_to_mindmohring
2001-02-01- coqc : option -imagefilliatr
2001-01-31Bug localisation des Syntactif Definitionherbelin
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des const...filliatr
2001-01-30Prise en compte du let-in dans lookup_*_as_renamedherbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2001-01-19Nouveaux bugs instanciation d'evar par des evarherbelin
2001-01-11Bug environnementherbelin
2001-01-04Rajout de la restriction de l'instance en cas d'unification de 2 variables ex...herbelin
2001-01-03Rattrapage d'erreur pour le Case + Eval Compute in pour Definitiondelahaye
2000-12-26Bug de contextesherbelin
2000-12-26Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...herbelin
2000-12-26Pattern sera mieux dans Pretyping; relâchement head_pattern_boundherbelin
2000-12-25Un nom long pour les variables de section qui font classe ou coercion; réorg...herbelin
2000-12-25Bug vieux Matchherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 15:10:09 +0000