aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2000-11-20Tables séparées pour chaque type de globalherbelin
2000-11-20Ajout sp_of_global; Introduction constant_path = section_pathherbelin
2000-11-20Introduction constant_path = section_pathherbelin
2000-11-20Ajout erreur GlobalNotFoundherbelin
2000-11-11Code more concernant feu les abstractionsherbelin
2000-11-10Code mortherbelin
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
2000-11-07Bug sur précédent commitherbelin
2000-11-07Nettoyage Names suiteherbelin
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...herbelin
2000-11-06nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...filliatr
2000-11-02correction Abstract (et make world passe!)filliatr
2000-11-02suppression des (* open Generic *)filliatr
2000-10-31- simplification Makefile (compilation des fichiers .ml'; pas encore parfaitfilliatr
2000-10-26Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ...herbelin
2000-10-24un espaceherbelin
2000-10-24Bug réduction suite modifs let-inherbelin
2000-10-23La réduction du Let s'appelle maintenant zeta comme dans le lambda-mu-calculherbelin
2000-10-23Simplifications/questionsherbelin
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18docherbelin
2000-10-18Renommage canonique :herbelin
2000-10-18Correction pb de globalisation dans print_mutualherbelin
2000-10-11Idem pour défs locales dans Varherbelin
2000-10-11Nouveau type rec_declarationherbelin
2000-10-11Delta des défs locales en de Bruijn toujours pas stableherbelin
2000-10-11Ajout push_rec_typesherbelin
2000-10-11Ajout mind_arities_envherbelin
2000-10-11Renommage des find_m*typeherbelin
2000-10-11Prise en compte de l'environnement dans les tests de bonne fondaisonherbelin
2000-10-11Prise en compte de l'environnement dans les tests de correction des inductifsherbelin
2000-10-11Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)herbelin
2000-10-11Prise en compte de Let dans build_dependent_inductiveherbelin
2000-10-10Messages d'erreurs Casesherbelin
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
2000-10-06Bug splay_prod_assumherbelin
2000-10-06MAJ pr_uniherbelin
2000-10-06correction bug univers (dummy_univ)filliatr
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 20:42:03 +0000