More concise defined evaluations (Definition arch : nat := Eval ... )

[andrew-appel]

An anonymous referee of a CoqPL submission suggests,

VST/lib/proof/spec_math.v

Line 31 in 6bcedd6

Definition arch : nat := ltac:(let x := constr:(arch') in let x := eval compute in x in exact x).

Why not

Definition arch : nat := Eval vm_compute in arch'.

same for GNU_errors just below