Prval vs val: is there still a difference in ATS2?

[Yannick Duchêne]

ATS2 recognize the keyword `prval`. Seems in old ATS1 programs, `prval` was, as its name suggest, used to hold proof variables. With ATS2, seems `val` can be substituted for `prval`.

Is this just that I met a special case where it works or is this ATS2 not requiring any‑more to use `prval`?

If the answer is yes, then is this related to some other similar changes which one should know?

[gmhwxi]

If you just do typechecking, then 'prval' can be replaced with 'val'.
After typechecking, 'prval' is erased but 'val' is not.