The following functions let us run MetaM actions in the context of a rapp or
goal. Rapps save the metavariable context in which they were run by storing a
Meta.SavedState. When we, for example, apply a rule to a goal, we run the
rule's action in the metavariable context of the goal (which is the
metavariable context of the goal's parent rapp). The resulting metavariable
context, in which the goal mvar is assigned to an expression generated by the
rule, then becomes the metavariable context of the rule's rapp.
To save and restore metavariable contexts, we use the MonadBacktrack MetaM
instance. This means that some elements of the state are persistent, notably
caches and trace messages. These become part of the global state.
The environment is not persistent. This means that modifications of the environment made by a rule are not visible in the global state and are reset once the tactic exits. As a result, rules which modify the environment are likely to fail.