summaryrefslogtreecommitdiff
path: root/lib/elf.c
diff options
context:
space:
mode:
authorThomas Bauereiss2019-01-17 01:20:33 +0000
committerThomas Bauereiss2019-01-17 01:20:33 +0000
commit7ebe7fe5a37959b9004548b4287dbfc1f6faa087 (patch)
treeebb50f11d57eb1e95a492c7be1b5dd8e51b7e86e /lib/elf.c
parent63fa9e0e2807e4b5fc3f825e6914a2fab5de37e3 (diff)
Work around an issue with type abbreviations in HOL
If we use the bitlist representation of bitvectors, the type argument in type abbreviations such as "bits('n)" becomes dead, which confuses HOL; as a workaround, expand type synonyms in this case.
Diffstat (limited to 'lib/elf.c')
0 files changed, 0 insertions, 0 deletions