1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74

(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors  Copyright 19992018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** This module defines potentially focussing tactics. They are used by Ltac to
emulate the historical behaviour of alwaysfocussed 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
focussed goals. This is a monad. *)
(** {5 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. *)
(** {5 Operations} *)
val lift : 'a Proofview.tactic > 'a t
(** Transform a tactic into a focussing tactic. The resulting tactic is not
focussed. *)
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 focussed, then the continuation is evaluated once.
Otherwise it is called in each of the currently focussed goals. *)
(** {5 Focussing} *)
val nf_enter : (Proofview.Goal.t > 'a t) > 'a t
(** Enter a goal. The resulting tactic is focussed. *)
val enter : (Proofview.Goal.t > 'a t) > 'a t
(** Enter a goal, without evar normalization. The resulting tactic is
focussed. *)
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. *)
(** {5 Notations} *)
val (>>=) : 'a t > ('a > 'b t) > 'b t
(** Notation for {!bind}. *)
val (<*>) : unit t > 'a t > 'a t
(** Sequence. *)
(** {5 List operations} *)
module List : Monad.ListS with type 'a t := 'a t
(** {5 Notations} *)
module Notations :
sig
val (>>=) : 'a t > ('a > 'b t) > 'b t
val (<*>) : unit t > 'a t > 'a t
end
