diff options
| author | Hugo Herbelin | 2016-10-10 12:12:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-03 14:40:35 +0100 |
| commit | b453d0281db6de0c36cbd9f2c0a094946f4fcfd6 (patch) | |
| tree | ed3ecb98fde5ca9a43583b25cff8ad719c9c1871 /kernel/nativecode.mli | |
| parent | 7497d4129775d15cdce862a0ac681c6400aabe54 (diff) | |
Slightly unifying renaming in ChoiceFacts.v.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions