The type of focussing tactics. A focussing tactic is like a normal tactic, except that it is able to remember it have entered a goal. Whenever this is the case, each subsequent effect of the tactic is dispatched on the focused goals. This is a monad.

The unit of the monad.

The bind of the monad.

Transform a tactic into a focussing tactic. The resulting tactic is not focused.

Given a continuation producing a tactic, evaluates the focussing tactic. If the tactic has not focused, then the continuation is evaluated once. Otherwise it is called in each of the currently focused goals.

Enter a goal, without evar normalization. The resulting tactic is focused.

with_env t returns, in addition to the return type of t, an environment, which is the global environment if t does not focus on goals, or the local goal environment if t focuses on goals.

Notation for bind.

Sequence.