Proofview.tactic to string or Pp.t

Developing plugins
1

Is there a way to print a Proofview.tactic as an Ltac expression?

2

Nope. A 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.

3

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 Proofview.tactic?

4

You can do that in several steps, in reverse order:

  • Evaluating a globalized Ltac with Tacinterp.eval_tactic
  • Globalize a raw Ltac with Tacintern.intern_pure_tactic
  • Parse a string with Pcoq.parse_string + Pltac.tactic

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.