aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-07-21retablissement minicoq (pour Jacek)filliatr
2000-07-19Quelques (*i*) pour ne pas casser oczmlwebcoq
2000-07-01Plus de env et sigma dans get_arity, plus de sigma dans make_arityherbelin
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter le...herbelin
2000-07-01Ajout fonctions sur les aritésherbelin
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter le...herbelin
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
2000-06-29Relative prend sigma en plus pour la normalisation du message d'erreurherbelin
2000-06-29Broutillesherbelin
2000-06-29Ajout make_typed_lazyherbelin
2000-06-29Normalisation des Evar avant génération des erreursherbelin
2000-06-21bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...filliatr
2000-06-09Docherbelin
2000-06-03Diversherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:05:45 +0000