diff options
| author | Gaëtan Gilbert | 2019-11-22 15:56:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-26 14:11:32 +0100 |
| commit | 836cc0361cd3df76beeeb3178cc6f7d8e0fed388 (patch) | |
| tree | 1f6b08e508a91912ec08052d6ce6687fb90599ea /interp/notation_ops.ml | |
| parent | d7879b8566e48aabfdbee5c27bd4c29691352233 (diff) | |
coercion functions are never called without a term to coerce
(inh_conv_coerces_to is unused so we remove it)
This makes the code simpler, removing dead match branches and Option.maps/gets
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions