package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

Enter a goal. The resulting tactic is focused.

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct