aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* 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
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
* Renommage AppL en AppGravatar herbelin2000-10-01
* whd_castapp_stack va de Term dans ReductionGravatar herbelin2000-10-01
* Suppression de ensure_applGravatar herbelin2000-10-01
* Bug message erreurGravatar herbelin2000-10-01
* Code comateuxGravatar herbelin2000-10-01
* Passage de la structure DOPN, DOP2, ... à une structure exprimant directemen...Gravatar herbelin2000-10-01
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
* Retrait de whd_ise1_metasGravatar herbelin2000-09-26
* On laisse les LetIn dans les types des constructeurs et des éliminationsGravatar herbelin2000-09-15
* CommentairesGravatar herbelin2000-09-15
* Minor correction for Ocamlweb + doc updateGravatar coq2000-09-14
* Abstraction de constrGravatar herbelin2000-09-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 20:50:25 +0000