aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Intv.v
Commit message (Collapse)AuthorAgeFilesLines
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-0/+319
- Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e