diff options
| author | Pierre-Marie Pédrot | 2020-07-13 15:02:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-06 12:33:58 +0200 |
| commit | 7126990e5b04d51927f414b277124c127fb14887 (patch) | |
| tree | aeffc105a7e498d1db244a30facbbfd09fab8c9d /plugins/syntax/float_syntax.ml | |
| parent | 8076de05c67a4dabc99233d8e2b81809c28794e4 (diff) | |
Actually use the default instance stored inside named_context_val.
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions