fix: fix bug in TacticInfo.getUsedConstantsAsSet

[adamtopaz]

The function TacticInfo.getUsedConstantsAsSet previously simply looked at the mvarids in the goals before a given tactic, check if they had an assignment, and collect the used constants from those assignments. For tactics that introduce new mvars internally, this approach missed some constants. For example, rw [h1,h2] should pick up both h1 and h2, while the previous approach only picked up h1.

This PR redefines TacticInfo.getUsedConstantsAsSet by collecting the used constants at the first level, as before, but also recursing into any mvars that appear in the assignment of the mvar. A test with a rw [Nat.add_assoc, Nat.add_comm y, h1] is also added, where the expected behavior is that Nat.add_assoc, Nat.add_comm and h1 should all be picked up as used constants.

Note: the proper way to handle this is probably to instantiate mvars inside of the MetaM monad, then collect the used constants. But this approach would require a much bigger refactor, since most of the code in this repo around TactcInfo doesn't run in the appropriate monad.