diff options
| author | Jasper Hugunin | 2020-08-21 16:58:28 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-08-25 13:53:30 -0700 |
| commit | 560b2888ffb414ae711b6158b5506ed79d6e039d (patch) | |
| tree | fbd1e53e14396886eca1bbc5bdf4e421261bc279 /plugins/syntax/float_syntax_plugin.mlpack | |
| parent | 51c0d56a5b0384e2f6bd980a1111547641c66b3e (diff) | |
Modify Init/Peano.v to compile with -mangle-names.
Here I added intros rather than moving premises before the colon,
partly to be more consistent with nearby lemma statements.
Diffstat (limited to 'plugins/syntax/float_syntax_plugin.mlpack')
0 files changed, 0 insertions, 0 deletions