aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-05-01 17:24:29 +0200
committerPierre-Marie Pédrot2017-05-01 17:28:26 +0200
commit2553e4bf5735a2bd127832e2d26609c6a8096fb7 (patch)
treed0c49dabac9cdc05911c5ffae213c3938430fada /interp/implicit_quantifiers.ml
parent991b78fd9627ee76f1a1a39b8460bf361c6af53d (diff)
Removing dead code in Autorewrite.
Since 260965d, an imperative code was semantically the identity because the closure allocation was not performed at the right moment. Because of it intricacy, I cannot really tell the original motivations of this piece of code, although it looks like it was for there for pretty-printing of errors. Anyway, both because the code was dubious and its effect not observed, it cannot hurt to remove it.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions