aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spGravatar herbelin2000-11-23
* Ajout push_rels_assumGravatar herbelin2000-11-23
* Reparation IsMutConstruct + TransparentGravatar mohring2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* deplacement poly_args; iterateurs sur les segmentsGravatar filliatr2000-11-22
* Reparation bug mutuels indGravatar mohring2000-11-22
* Ajout d'une fonction pour recuperer la liste des constantesGravatar delahaye2000-11-21
* implicites manuelsGravatar filliatr2000-11-21
* Tables séparées pour chaque type de globalGravatar herbelin2000-11-20
* Ajout sp_of_global; Introduction constant_path = section_pathGravatar herbelin2000-11-20
* Introduction constant_path = section_pathGravatar herbelin2000-11-20
* Ajout erreur GlobalNotFoundGravatar herbelin2000-11-20
* Code more concernant feu les abstractionsGravatar herbelin2000-11-11
* Code mortGravatar herbelin2000-11-10
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* Bug sur précédent commitGravatar herbelin2000-11-07
* Nettoyage Names suiteGravatar herbelin2000-11-07
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* - simplification Makefile (compilation des fichiers .ml'; pas encore parfaitGravatar filliatr2000-10-31
* Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ...Gravatar herbelin2000-10-26
* un espaceGravatar herbelin2000-10-24
* Bug réduction suite modifs let-inGravatar herbelin2000-10-24
* La réduction du Let s'appelle maintenant zeta comme dans le lambda-mu-calculGravatar herbelin2000-10-23
* Simplifications/questionsGravatar herbelin2000-10-23
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* docGravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Correction pb de globalisation dans print_mutualGravatar herbelin2000-10-18
* Idem pour défs locales dans VarGravatar herbelin2000-10-11
* Nouveau type rec_declarationGravatar herbelin2000-10-11
* Delta des défs locales en de Bruijn toujours pas stableGravatar herbelin2000-10-11
* Ajout push_rec_typesGravatar herbelin2000-10-11
* Ajout mind_arities_envGravatar herbelin2000-10-11
* Renommage des find_m*typeGravatar herbelin2000-10-11
* Prise en compte de l'environnement dans les tests de bonne fondaisonGravatar herbelin2000-10-11
* Prise en compte de l'environnement dans les tests de correction des inductifsGravatar herbelin2000-10-11
* Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)Gravatar herbelin2000-10-11
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Messages d'erreurs CasesGravatar herbelin2000-10-10
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Bug splay_prod_assumGravatar herbelin2000-10-06
* MAJ pr_uniGravatar herbelin2000-10-06
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
* Mise en conformité nouveau Simpl pour FixGravatar herbelin2000-10-04
* Touche finale à la réduction du let in dans conv et closureGravatar herbelin2000-10-04
* Elimination des coupures sur le type constantGravatar herbelin2000-10-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 06:10:10 +0000