aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2000-06-03Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constrherbelin
2000-06-02Retrait de decomp_prod non conforme à sa specherbelin
2000-06-02Retrait de certains castsherbelin
2000-06-02docherbelin
2000-06-02Bug DLAM dans strongherbelin
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-31Nettoyage de Genericherbelin
2000-05-31Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursherbelin
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans l...herbelin
2000-05-25Bug existential_value au lieu de existential_type + divers sur existentialherbelin
2000-05-22Commentairesherbelin
2000-05-22Renommage hypothèses de nom redondant dans les environnementsherbelin
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
2000-05-22Changement nom module Constant en Declarationsherbelin
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18MAJ modifs Inductiveherbelin
2000-05-18Ajouts des causes d'erreur de Indrecherbelin
2000-05-18Restructuration des outils pour les inductifs.herbelin
2000-05-18Ajout lift_contextherbelin
2000-05-18Effets de bords suite à la restructuration des inductives (cf Inductive)herbelin
2000-05-18Centralisation prod_name and co dans Environ; mkLambda_string dans Termherbelin
2000-05-18Restructuration des outils pour les inductifs.herbelin
2000-05-18Centralisation prod_name and co dans Environ; mkLambda_string dans Termherbelin
2000-05-16Ajout mis_typepathherbelin
2000-05-05docherbelin
2000-05-05Ajout d'un strong 'light'herbelin
2000-05-04Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)herbelin
2000-05-03Retrait de PrintConstr vers top_printersdelahaye
2000-05-03diverses modifs pour ocamlwebfilliatr
2000-05-03Ajout du langage de tactiquesdelahaye
2000-05-02Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'herbelin
2000-04-28Déplacement du type reference dans Termherbelin
2000-04-28Déplacement du type reference dans Termherbelin
2000-04-27Retrait fullmind de inductive_summary pour simplicitéherbelin
2000-04-26Commentairesherbelin
2000-04-21Sign.db_signature is now an abstract typecourant
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
2000-03-30erreurs lexicales dans les patterns (manquait des espaces)filliatr
2000-03-21Modification de type_of_case, type_case_branches, etcherbelin
2000-03-21Ajout {prod,lambda}_nameherbelin
2000-03-21Déplacement fonction du discharge dans Dischargeherbelin
2000-03-21Plus besoin de env dans reduce_mind_case; make_arity et make_constructor sort...herbelin
2000-03-21Prise en compte nouveau case_info dans type_caseherbelin
2000-03-21Prise en compte nouveau case_infoherbelin
2000-03-21Ajout des fonctions de formation du 'case_info'; Suppression de make_arity et...herbelin
2000-03-21Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...herbelin
2000-03-20Tautofilliatr
2000-03-20Bug ordre des inductifs mutuelsherbelin
2000-03-17Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'herbelin
2000-03-17Un cast inutileherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 14:55:11 +0000