I find it very handy to have the AST of
constr around for writing tactics. However, it is a little unnerving that
kind is placed under the
In what sense is it unsafe? Will it cause coq to crash or make my proof unsound?
I saw functions such as
is_constructor are exported as safe functions. My guess is that as long as I don’t use the AST to construct terms but only traverse/read the AST as an extension of pattern matching, I shouldn’t run into any issues. Is that correct?