# Module `Ftactic`

This module defines potentially focussing tactics. They are used by Ltac to emulate the historical behaviour of always-focussed tactics while still allowing to remain global when the goal is not needed.

`type +'a focus`

`type +'a t`

`= 'a focus Proofview.tactic`

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.

###### Monadic interface

`val return : 'a -> 'a t`

The unit of the monad.

###### Operations

`val lift : 'a Proofview.tactic -> 'a t`

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

`val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic`

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.

###### Focussing

`val enter : (Proofview.Goal.t -> 'a t) -> 'a t`

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

`val with_env : 'a t -> (Environ.env * 'a) t`

`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.

###### Notations

###### List operations

`module List : Monad.ListS with type 'a t := 'a t`

###### Notations

`module Notations : sig ... end`