bad error message when Clight import missing
Closed this issue · 1 comments
andrew-appel commented
Consider this proof development:
Require Import VST.floyd.proofauto.
#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
The user has forgotten to Require Import the .v file containing the Clight AST produced by clightgen. The error message is,
Variable prog should be bound to a term but is bound to a intropattern.
which is not very helpful.
andrew-appel commented
Fixed in by P.R. 564