at/old operator never used should perhaps be a warning
Hello,
On the following code:
module Toto
val f (x : int) : int
ensures { result = old x }
end
I get an error:
this `at'/`old' operator is never used
I think this error should only be a warning. Also, is there a flag to make it disappear ?
Also, it would be cool if the error could mention "old" instead of `old' (which I don't know about). And make the distinction between at and old if possible:
"Warning: this "old" operator is never used"