aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/instantiate.ml
Commit message (Expand)AuthorAge
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Généralisation de constant_opt_value en reference_opt_valueGravatar herbelin2000-11-27
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* 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
* Abstraction de constrGravatar herbelin2000-09-14
* 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
* Nettoyage de GenericGravatar herbelin2000-05-31
* 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
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Export mis_typed_arityGravatar herbelin2000-03-07
* - constantes avec recettesGravatar filliatr1999-12-09
* Backtrack sur modif Evd.evd_conclGravatar herbelin1999-11-25
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* les variables existentielles contiennent maintenant un environnement (typeGravatar filliatr1999-10-19
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* module LogicGravatar filliatr1999-10-14
* plus de recettes pour les corps des constantesGravatar filliatr1999-10-13
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
* ajout des inductifs (sans types singletons pour l'instant)Gravatar filliatr1999-08-30
* modules Instantiate, Constant et InductiveGravatar filliatr1999-08-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 00:11:46 +0000