diff options
| author | Jasper Hugunin | 2020-10-09 16:54:33 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-11 19:05:14 -0700 |
| commit | 44b13a7a3c5c849e6aca9a1f0a5e6aa0909fa651 (patch) | |
| tree | aac905f3cfb2dc67f5e70f2023da2ed520bf3dd8 /kernel/nativecode.ml | |
| parent | 3c5ff2175d0711da2dca1259b953f308cd5d82ae (diff) | |
Modify NArith/Ndigits.v to compile with -mangle-names
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions