aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
Commit message (Expand)AuthorAge
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
* N'importe quel rawconstr maintenant dans le contexte d'une référenceGravatar herbelin2000-04-26
* Prise en compte nouveau case_infoGravatar herbelin2000-03-21
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* Traduction constr->rawconstr (avant dans TermastGravatar herbelin2000-01-07