aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.ml
Commit message (Expand)AuthorAge
* MAJ commentairesGravatar herbelin2000-12-14
* Reparation conditions de positivites inductifs, echange dans add_entryGravatar mohring2000-12-06
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
* Bug dans la gestion du contexte en présence de Fix dans le calcul de gardeGravatar herbelin2000-11-27
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Prise en compte de l'environnement dans les tests de bonne fondaisonGravatar herbelin2000-10-11
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01
* Bug message erreurGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* 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
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Plus de env et sigma dans get_arity, plus de sigma dans make_arityGravatar herbelin2000-07-01
* Extension de find_inductive aux co-inductifs et renommage en find_rectypeGravatar herbelin2000-07-01
* BroutillesGravatar herbelin2000-06-29
* Retrait de certains castsGravatar 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
* 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
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
* Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)Gravatar herbelin2000-05-04
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Modification de type_of_case, type_case_branches, etcGravatar herbelin2000-03-21
* Prise en compte nouveau case_info dans type_caseGravatar herbelin2000-03-21
* Un cast inutileGravatar herbelin2000-03-17
* RedondancesGravatar herbelin2000-03-07
* 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
* Discharge (encore bugge)Gravatar filliatr1999-12-09
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* correction bug construct_referenceGravatar filliatr1999-12-07
* declarations eliminations / debuggae inductifs (debut)Gravatar filliatr1999-12-06
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* poursuite de VernacentriesGravatar filliatr1999-12-01
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* Backtrack sur modif Evd.evd_conclGravatar herbelin1999-11-25
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 18:14:59 +0000