aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/ClightBigstep.v
Commit message (Expand)AuthorAgeFilesLines
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Merge of the clightgen branch:xleroy2012-12-291-9/+9
* Clight: split off the big step semantics in ClightBigstep.xleroy2012-10-141-0/+583