aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2000-11-26Prise en compte de noms absolus dans la nametabherbelin
2000-11-24Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabfilliatr
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
2000-11-23Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spherbelin
2000-11-23Ajout push_rels_assumherbelin
2000-11-23Reparation IsMutConstruct + Transparentmohring
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...herbelin
2000-11-22deplacement poly_args; iterateurs sur les segmentsfilliatr
2000-11-22Reparation bug mutuels indmohring
2000-11-21Ajout d'une fonction pour recuperer la liste des constantesdelahaye
2000-11-21implicites manuelsfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:07:29 +0000