[vernac] Interpret regular vernacs symbolically

This provides uniformity to the inner loop and prepares the way to
export a refined type for interpretation.

The only non-uniformity remaining is the one due to the `?proof`
parameter; it won't be easy to fix due to upper layers issues.

Note that this step is not yet fully satisfying, as a true typed
`vernac_expr` definition is still not possible because of syntactic
non-uniformity, in particular all the surgery done for `CoFixpoint`
and `Instance` should be eliminated in favor of more refined AST tags.

An interesting TODO is to handle attributes symbolically too, as to
remove boilerplate.

0 files changed, 0 insertions, 0 deletions