-
LocalContextcontainsLocalDecls, and is owned by aMetavar. -
MetavarContextcontainsMetavars, and is owned by aMetaM. -
TacticMcontains the list of goal[goal : MVarId].
LocalContext contains LocalDecls, and is owned by a Metavar. MetavarContext contains Metavars, and is owned by a MetaM. TacticM contains the list of goal [goal : MVarId].