Is there a way to print a Proofview.tactic as an Ltac expression?
Proofview.tactic is a semantic construct, that can be generated by arbitrary ML code, so in general there is no Ltac expression from which it stems.
Bummer! To clarify my intentions, I need some way of pairing
Proofview.tactics with their names. My plugin currently accepts both a tactic expression and its string representation as arguments. I would prefer to have only one of those arguments, so do you suppose the other direction is possible? I.e., parsing a tactic string and producing a
You can do that in several steps, in reverse order:
- Evaluating a globalized Ltac with
- Globalize a raw Ltac with
- Parse a string with
The most stable representation for a Ltac expression would be its globalized form, so I’d aim for this as the intermediate representation of choice. You can even print it.