diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-05-01 17:24:29 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-05-01 17:28:26 +0200 |
commit | 2553e4bf5735a2bd127832e2d26609c6a8096fb7 (patch) | |
tree | d0c49dabac9cdc05911c5ffae213c3938430fada /theories/Sorting | |
parent | 991b78fd9627ee76f1a1a39b8460bf361c6af53d (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 'theories/Sorting')
0 files changed, 0 insertions, 0 deletions