diff options
| author | Jasper Hugunin | 2020-09-09 10:41:35 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | 2128f623d1d9f26b5791d65e95c8d624ac7e48b9 (patch) | |
| tree | 4ee6dd5d20b592aa4963c4f94f64e9913d0c0bea /plugins/syntax/float_syntax.ml | |
| parent | 6b677ba003748f6222539a083e9de7d47a60c373 (diff) | |
Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-names
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions