Best way to monkeypatch existing tactics?

Stream: metaprogramming / tactics

[Lawrence Wu (llllvvuu)]

Suppose there's some tactic from the library (say, wlog), that I want to add some behavior to (but still run the original implementation), e.g. maybe I want to do something like (pseudocode)

redefine wlog foo generalizing bar :=
  dbg_trace "hello"
  wlog foo generalizing bar
  dbg_trace "goodbye"

Is there a generally recommended way to make these kind of monkeypatches?

[Kyle Miller]

No, I believe there's no mechanism for this. I'm sure there are some creative hacks to simulate it, but there's no general system to call the previous implementation of a tactic.