diff options
| author | Emilio Jesus Gallego Arias | 2020-11-16 04:05:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2021-02-25 20:55:20 +0100 |
| commit | d866ed978ece3b80364dfcf67ee801a556462f29 (patch) | |
| tree | aa11a82739c65d6b54d220485d4131e561ee0f91 /kernel/genOpcodeFiles.ml | |
| parent | 24e94b3dac66510e6d57b9f55f9a4e3e84fd6e54 (diff) | |
[proof using] Remove duplicate code, refactor.
PR #13183 introduced quite a bit of duplicate code, we refactor it and
expose less internals on the way. That should make the API more
robust.
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions