summaryrefslogtreecommitdiff
path: root/common/Unityping.v
Commit message (Expand)AuthorAge
* Merge of branch linear-typing:Gravatar xleroy2014-04-06
* Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):Gravatar xleroy2014-03-28
* Revised division of labor between RTLtyping and Lineartyping:Gravatar xleroy2014-03-27