aboutsummaryrefslogtreecommitdiff
path: root/pretyping/detyping.ml
AgeCommit message (Expand)Author
2000-05-02Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'herbelin
2000-04-28Changement de représentation du contexte des réf dans rawconstr et patternherbelin
2000-04-26N'importe quel rawconstr maintenant dans le contexte d'une référenceherbelin
2000-03-21Prise en compte nouveau case_infoherbelin
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration d...herbelin
2000-01-07Traduction constr->rawconstr (avant dans Termastherbelin