blob: c108c0c2ea2523f881527caeacd16e6b26ed7d62 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** 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
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 : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t
(** Enter a goal. The resulting tactic is focussed. *)
val enter : ([ `LZ ] 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
|
