diff options
| author | Gaëtan Gilbert | 2020-05-20 13:32:56 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-20 13:32:56 +0200 |
| commit | a87e04684335d276cb52c6f8c7385f9549194aef (patch) | |
| tree | ab14c92d9b458b7b9aae8f831ca0c91db42d62dd /plugins/syntax/float_syntax.ml | |
| parent | 7163b75641bb8bf0a88856f43e536a9fba0d6ae7 (diff) | |
| parent | 0643873397552cc2fe4d1486c14f206968dea672 (diff) | |
Merge PR #12356: [declare] Remove unused parameters in prepare_obligation
Reviewed-by: SkySkimmer
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions