summaryrefslogtreecommitdiff
path: root/common/Unityping.v
Commit message (Expand)AuthorAge
* Revised division of labor between RTLtyping and Lineartyping:Gravatar xleroy2014-03-27