aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2001-03-14Prise en compte des Let dans l'instance des evarsherbelin
2001-03-12Amélioration message d'erreur conditions de gardeherbelin
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
2001-03-08corrections de bug de la reductionbarras
2001-03-08compare_constr independent du groupement des applications.barras
2001-03-06réparation (?) discharge axiomefilliatr
2001-03-05Re-Déplacement extended_rel_listherbelin
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-03-01nouvelle implantation de la reductionbarras
2001-02-28retire profilemohring
2001-02-28Changement de subst_metamohring
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2001-02-08simplification du make depend; fonctions de stat. util. memoire dans certains...filliatr
2001-02-07Chgt signature de type_of_existentialherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des const...filliatr
2001-01-31Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...herbelin
2001-01-27make docherbelin
2001-01-27Ajout alias mutual_inductive_path = section_pathherbelin
2001-01-24Ajout global_vars_declherbelin
2001-01-24Docherbelin
2000-12-26Déplacement du type stack de Reduction vers Closure et utilisation pour accÃ...herbelin
2000-12-25Alias variable_pathherbelin
2000-12-20Bug mauvais environnement dans le test d'eta-conversionherbelin
2000-12-18Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_nameherbelin
2000-12-15Le bon choix, c'est finalement identifier = stringherbelin
2000-12-15Mise en place d'un module Ident avec test de l'efficacité quand identifier=s...herbelin
2000-12-15 - suppression mind_extract_paramsfilliatr
2000-12-15Petite réorganisationherbelin
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif d'u...herbelin
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif d'u...herbelin
2000-12-14MAJ commentairesherbelin
2000-12-14Raffinement erreur Wrong Predicateherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-12-06Reparation conditions de positivites inductifs, echange dans add_entrymohring
2000-12-05Mini-nettoyage noms longsherbelin
2000-11-29Prise en compte de la contrainte de type dans Definition comme étant un cast...herbelin
2000-11-29Ajout d'un test pour vérifier qu'on a affaire à un identherbelin
2000-11-29Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageherbelin
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath po...herbelin
2000-11-27Faut-il mettre la réduction let-in dans la réduction unfold ?herbelin
2000-11-27On déplie les locaux dans les types plutôt que de les quantifier par un Letherbelin
2000-11-27Utilisation de Let In pour les constantes locales, prise en compte des Let In...herbelin
2000-11-27Bug dans la gestion du contexte en présence de Fix dans le calcul de gardeherbelin
2000-11-27Prise en compte des let in dans les instances de globauxherbelin
2000-11-27Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...herbelin
2000-11-27Ajout map_constr_with_full_binders et strong pour Simplherbelin
2000-11-27Généralisation de constant_opt_value en reference_opt_valueherbelin
2000-11-27Bug dans le calcul des dépendances dans add_discharged_constantherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:11:08 +0000