aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Intv.v
Commit message (Collapse)AuthorAgeFilesLines
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-5/+1
| | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-23/+23
|
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-4/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* 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