aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
2000-12-25Bug prédicatherbelin
2000-12-20Bug prédicat old Case/Matchherbelin
2000-12-20Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...herbelin
2000-12-19Export fonction testant si un inductive est un recordherbelin
2000-12-18Amélioration message d'erreur mauvais prédicatherbelin
2000-12-18Debut de nettoyage de Simplmohring
2000-12-16Suppression du warning several default clausesherbelin
2000-12-15Bug env vis à vis du let inherbelin
2000-12-15Bugs calcul du prédicat des Cases et Caseherbelin
2000-12-15Printermohring
2000-12-14Mauvais env donné à new_isevarherbelin
2000-12-14Oubli test de correction à l'instantiation des evarsherbelin
2000-12-14Mise en pageherbelin
2000-12-14LetIn dans Simplmohring
2000-12-14Raffinement erreur Wrong Predicateherbelin
2000-12-14Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases devien...herbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-12-12Hint Unfold Local + commentairesmohring
2000-12-11Debut de reparation de simplmohring
2000-12-05Bug Cases en presence d'une absence de clauseherbelin
2000-11-29Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageherbelin
2000-11-27La table de pré-évaluation des constantes ne doit pas persister au dischargeherbelin
2000-11-27Utilisation de Let In pour les constantes locales, prise en compte des Let In...herbelin
2000-11-27Branchement du mécanisme d'instantiation des Evar en présence de définitio...herbelin
2000-11-27Prise en compte des let-in dans les fonctions de réduction pour les tactiquesherbelin
2000-11-26Prise en compte de noms absolus dans la nametabherbelin
2000-11-26Remplacement de certains sp_of_id par des locateherbelin
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon S...filliatr
2000-11-24resolution implicites dans produits (bug)filliatr
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 20:17:11 +0000