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.

val bind : 'a t -> ('a -> 'b t) -> 'b t

The bind 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 nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
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
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t

Notation for bind.

val (<*>) : unit t -> 'a t -> 'a t

Sequence.

List operations
module List : Monad.ListS with type 'a t := 'a t
Notations
module Notations : sig ... end