aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
Commit message (Expand)AuthorAge
* réparation (?) discharge axiomeGravatar filliatr2001-03-06
* nouvelle implantation de la reductionGravatar barras2001-03-01
* Changement de subst_metaGravatar mohring2001-02-28
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* - suppression mind_extract_paramsGravatar filliatr2000-12-15
* Petite réorganisationGravatar herbelin2000-12-15
* Les params d'inductif deviennent en même temps propre à chaque inductif d'u...Gravatar herbelin2000-12-14
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Prise en compte de la contrainte de type dans Definition comme étant un cast...Gravatar herbelin2000-11-29
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
* Bug dans le calcul des dépendances dans add_discharged_constantGravatar herbelin2000-11-27
* Reparation bug mutuels indGravatar mohring2000-11-22
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* - simplification Makefile (compilation des fichiers .ml'; pas encore parfaitGravatar filliatr2000-10-31
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* retablissement minicoq (pour Jacek)Gravatar filliatr2000-07-21
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* BroutillesGravatar herbelin2000-06-29
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* CommentairesGravatar herbelin2000-04-26
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Prise en compte nouveau case_info dans type_caseGravatar herbelin2000-03-21
* Bug ordre des inductifs mutuelsGravatar herbelin2000-03-20
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Intégration initiale du CasesGravatar herbelin1999-12-11
* debug discharge et inductifsGravatar filliatr1999-12-10
* - constantes avec recettesGravatar filliatr1999-12-09
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* - environment -> safe_environmentGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 14:37:09 +0000