aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sorting
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-05-01 17:24:29 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-05-01 17:28:26 +0200
commit2553e4bf5735a2bd127832e2d26609c6a8096fb7 (patch)
treed0c49dabac9cdc05911c5ffae213c3938430fada /theories/Sorting
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 'theories/Sorting')
0 files changed, 0 insertions, 0 deletions