aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-05-05 18:09:30 +0200
committerMaxime Dénès2017-05-05 18:09:30 +0200
commita76a71eda10b054b04de4ff56f0637a32077edd4 (patch)
tree63d46cf1dc4446fec44ea61cb9a075f30204c5fb /interp/implicit_quantifiers.ml
parent2c5b74e0b45eb8a6a956e0bde13be16379b54714 (diff)
Remove two unused opens.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions