aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2000-10-04Touche finale à la réduction du let in dans conv et closureherbelin
2000-10-04Elimination des coupures sur le type constantherbelin
2000-10-03Rebranchement de la tactique Letherbelin
2000-10-01Renommage AppL en Appherbelin
2000-10-01whd_castapp_stack va de Term dans Reductionherbelin
2000-10-01Suppression de ensure_applherbelin
2000-10-01Bug message erreurherbelin
2000-10-01Code comateuxherbelin
2000-10-01Passage de la structure DOPN, DOP2, ... à une structure exprimant directemen...herbelin
2000-10-01Disparition du type oper mais nouveau type global_referenceherbelin
2000-09-26Retrait de whd_ise1_metasherbelin
2000-09-15On laisse les LetIn dans les types des constructeurs et des éliminationsherbelin
2000-09-15Commentairesherbelin
2000-09-14Minor correction for Ocamlweb + doc updatecoq
2000-09-14Abstraction de constrherbelin
2000-09-14Nouvelle version de frterm; ajout des contextes dans l'enviornnement de rédu...herbelin
2000-09-14Rendus obsolètes par le LetInherbelin
2000-09-14Abstraction de constrherbelin
2000-09-12Modification mkAppL; abstraction via kind_of_term; changement dans Reductionherbelin
2000-09-12Vers la paramétrisation des fonctions de Reduction et vers la fusion deherbelin
2000-09-10nettoyageherbelin
2000-09-10Correction pour make docherbelin
2000-09-10Suppression de Abstherbelin
2000-09-10Ajout d'un LetIn primitif.herbelin
2000-09-10Intégration à Termherbelin
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
2000-09-06Ajout erreur unexpected typeherbelin
2000-09-06kernel/type_errors.mlherbelin
2000-08-17Pattern matching de sous-termesdelahaye
2000-07-25retablissement make doc et make minicoqfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 04:54:57 +0000