diff options
| author | Jasper Hugunin | 2020-08-25 13:32:35 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:33 -0700 |
| commit | ea5f72382a1290028e1c41ad1548546d2040529b (patch) | |
| tree | dc2f6f1edf0d5d0c9e650b63a20a571486c6167f /doc/plugin_tutorial/tuto0/src/dune | |
| parent | 9a51c936136346b0a5ca5c81c17fb923a86a38ea (diff) | |
Modify Numbers/NatInt/NZMulOrder.v to compile with -mangle-names
Diffstat (limited to 'doc/plugin_tutorial/tuto0/src/dune')
0 files changed, 0 insertions, 0 deletions