Capturing metavariable assignment

Stream: metaprogramming / tactics

[Jannis Limperg]

For the proof search tactic I'm writing, I'd like to be able to capture and restore the current metavariable assignment. Specifically, I want to apply a tactic to a goal, do something with the produced subgoals, then later on backtrack to the state before the tactic was run. This backtracking should reset not only the goals but also any metavariables that were assigned by the tactic. Can I achieve this by just saving the tactic_state?

[Gabriel Ebner]

Yes.

[Jannis Limperg]

Wonderful, thanks!