Limit modifies terms

[pascutto]

consumes and modifies declarations currently accept any terms.
These should be restricted to qualified identifiers only e.g. x.y.z.

[backtracking]

Do we want to allow x.(old y).z?

[mariojppereira]

Do we want to allow x.(old y).z?

That is very interesting, indeed :) I believe this would make sense only for consumes, right? A modifies clause containing an old seems odd to me.

[backtracking]

Here is an example where modifies x.(old y).z would make sense:

type t = { mutable y: int ref }
let f (x: t) = x.y := 0; x.y <- ref 0