diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-27 20:25:21 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-27 20:25:21 +0200 |
commit | 78df4fe4fad46fee83f5044525fd8e530d8da6ff (patch) | |
tree | 8d6ceedc108c46053b2f966693fb0c2e439ae39f /common/Unityping.v | |
parent | 91ed1b752d2661478840e40a0d977b068d99490d (diff) | |
download | compcert-78df4fe4fad46fee83f5044525fd8e530d8da6ff.tar.gz compcert-78df4fe4fad46fee83f5044525fd8e530d8da6ff.zip |
More refactoring of the Debug Information.
In order to remove unnecessary dependecies the implemenation type is made
and the DebugInit file initializes the fields in the record. This allows
it to move more functions behind the Debug interface without introducing
circular dependencies.
Diffstat (limited to 'common/Unityping.v')
0 files changed, 0 insertions, 0 deletions