Get all metavariables which mvarId
depends on. These are the metavariables
which occur in the target or local context or delayed assignment (if any) of
mvarId
, plus the metavariables which occur in these metavariables, etc.
Instances For
auxiliary function for getUnassignedGoalMVarDependencies
auxiliary function for getUnassignedGoalMVarDependencies
Modifier recover
for a tactic (sequence) to debug cases where goals are closed incorrectly.
The tactic recover tacs
for a tactic (sequence) tacs applies the tactics and then adds goals
that are not closed starting from the original