diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-09 03:39:07 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:34:31 +0200 |
| commit | 7058b9b400e252a30c1e624cbe0de26b70356d64 (patch) | |
| tree | 5115f5af4231761a484e0413f4179423e183ca9a /interp/constrexpr_ops.ml | |
| parent | ee2197096fe75a63b4d92cb3a1bb05122c5c625b (diff) | |
[location] Cleanup.
We remove some unnecessary functions introduced before in the patch
series + unused functions.
Diffstat (limited to 'interp/constrexpr_ops.ml')
0 files changed, 0 insertions, 0 deletions