aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Initializersproof.v
Commit message (Expand)AuthorAgeFilesLines
* Improved semantics of castsxleroy2011-07-171-9/+8
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to the...xleroy2011-07-161-63/+40
* Merge of branch "unsigned-offsets":xleroy2011-04-091-2/+3
* Incompatibility 8.3 / 8.3pl1xleroy2011-03-141-1/+1
* Slightly nicer semantics for initializationxleroy2011-03-131-28/+29
* More global initialization work done and proved in Coq.xleroy2011-03-131-12/+312
* Initializers for global variables: compile-time evaluation of expressions don...xleroy2011-03-121-0/+555