feat: Tactic steps now include used constants

[adamtopaz]

When the repl responds with a tactic step, the response will now include an array with the names of the constants used in the step.

Implementation details: Given a tactic info i : TacticInfo, we calculate the used constants as follows:

• Look at the mvarid's in i.goalsBefore, and focus on those which have been assigned in i.mctxAfter.
• Look at each such assignment, and collect the used constants as a NameSet.
• Take the union of all these NameSets, and convert the result to an array.

In the future it would be better to give the user an option of whether or not to include the used constants, but having a more robust configuration system for the whole package would probably be the way to go.