aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* 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
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* Relative prend sigma en plus pour la normalisation du message d'erreurGravatar herbelin2000-06-29
* BroutillesGravatar herbelin2000-06-29
* Ajout make_typed_lazyGravatar herbelin2000-06-29
* Normalisation des Evar avant génération des erreursGravatar herbelin2000-06-29
* bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> .vo...Gravatar filliatr2000-06-21
* DocGravatar herbelin2000-06-09
* DiversGravatar herbelin2000-06-03
* Retrait des lam_and_pop and co; ajout d'un destructeur 'lispien' de constrGravatar herbelin2000-06-03
* Retrait de decomp_prod non conforme à sa specGravatar herbelin2000-06-02
* Retrait de certains castsGravatar herbelin2000-06-02
* docGravatar herbelin2000-06-02
* Bug DLAM dans strongGravatar herbelin2000-06-02
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Modification messages d'erreurs, possibilité de n'importe quel constr dans l...Gravatar herbelin2000-05-26
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
* CommentairesGravatar herbelin2000-05-22
* Renommage hypothèses de nom redondant dans les environnementsGravatar herbelin2000-05-22
* suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsGravatar herbelin2000-05-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-31 18:59:18 +0000