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

Google Group
1

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?

2

If you just do typechecking, then ‘prval’ can be replaced with ‘val’.
After typechecking, ‘prval’ is erased but ‘val’ is not.On Friday, August 8, 2014 4:11:58 AM UTC-4, Yannick Duchêne wrote:

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?