An anonymous referee of a CoqPL submission suggests, https://github.com/PrincetonUniversity/VST/blob/6bcedd6e987cea40fe577540782f88d85be687dd/lib/proof/spec_math.v#L31 Why not ```Coq Definition arch : nat := Eval vm_compute in arch'. ``` same for `GNU_errors` just below
An anonymous referee of a CoqPL submission suggests,
VST/lib/proof/spec_math.v
Line 31 in 6bcedd6
Why not
Definition arch : nat := Eval vm_compute in arch'.same for
GNU_errorsjust below