diff options
| author | Jasper Hugunin | 2020-08-25 13:05:49 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:32 -0700 |
| commit | 17ed93c2caadfcf3a2aee8f2b9683191063b2951 (patch) | |
| tree | fc8955ee8594e1de7b8a9edc4e699291c1e5c10c /kernel/typeops.ml | |
| parent | e5880b643bb9ce6974d3ecffd8edcbfad9f45cd4 (diff) | |
Modify Structures/Orders.v to compile with -mangle-names
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions