aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
...
* 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
* Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...Gravatar herbelin2000-09-14
* Rendus obsolètes par le LetInGravatar herbelin2000-09-14
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Vers la paramétrisation des fonctions de Reduction et vers la fusion deGravatar herbelin2000-09-12
* nettoyageGravatar herbelin2000-09-10
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Intégration à TermGravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* Ajout erreur unexpected typeGravatar herbelin2000-09-06
* kernel/type_errors.mlGravatar herbelin2000-09-06
* Pattern matching de sous-termesGravatar delahaye2000-08-17
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* retablissement minicoq (pour Jacek)Gravatar filliatr2000-07-21
* Quelques (*i*) pour ne pas casser oczmlwebGravatar coq2000-07-19
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* Ajout fonctions sur les aritésGravatar herbelin2000-07-01
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 04:29:40 +0000