aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/instantiate.mli
Commit message (Expand)AuthorAge
* 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
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Généralisation de constant_opt_value en reference_opt_valueGravatar herbelin2000-11-27
* 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
* Suppression de AbstGravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Bug existential_value au lieu de existential_type + divers sur existentialGravatar herbelin2000-05-25
* MAJ modifs InductiveGravatar herbelin2000-05-18
* 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
* - environment -> safe_environmentGravatar filliatr1999-12-01
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* module LogicGravatar filliatr1999-10-14
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
* ajout des inductifs (sans types singletons pour l'instant)Gravatar filliatr1999-08-30
* un petit effort de presentation dans les interfacesGravatar filliatr1999-08-30
* modules Instantiate, Constant et InductiveGravatar filliatr1999-08-25