aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-02-08 16:44:06 +0100
committerXavier Leroy <xavierleroy@users.noreply.github.com>2018-02-08 16:44:06 +0100
commitf80498e19a670040dce0795a8ea1cc83ca490ecc (patch)
tree158483ab5559938537983d8e2f1640457ddbfe47 /cfrontend/C2C.ml
parentf02f00a01b598567f70e138c144d9581973802e6 (diff)
downloadcompcert-f80498e19a670040dce0795a8ea1cc83ca490ecc.tar.gz
compcert-f80498e19a670040dce0795a8ea1cc83ca490ecc.zip
Extend the modorder tool to handle Coq files as well (#54)
This is useful to e.g. identify the .vo files from CompCert that a clightgen-generated .v file needs. Also: the "result" field of the record type is now initialized with the LHS of the dependency, not the RHS. It doesn't matter because the result field is unused, but it makes more sense now.
Diffstat (limited to 'cfrontend/C2C.ml')
0 files changed, 0 insertions, 0 deletions