The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I'd like to write a tactic as a plugin that roughly has this "type":

my_plugin_tac : (term -> (term -> tactic) -> tactic) -> tactic

i want the plugin to take a tactic, that takes a continuation to pass its result to so the ML plugin is going to supply the (term -> tactic) to its argument and use it to use the result.

Does anyone know how to do this? I've only passed constrs to tactics thus far, not tactic functions.

Thanks.

--

gregory malecha