blob: cf97955eed48e94985fa97ea1db96f0f57ec99e8 (
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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** This module defines proof facilities relevant to the
toplevel. In particular it defines the global proof
environment. *)
(** Type of proof modes :
- A name
- A function [set] to set it *from standard mode*
- A function [reset] to reset the *standard mode* from it
*)
type proof_mode = {
name : string ;
set : unit -> unit ;
reset : unit -> unit
}
(** Registers a new proof mode which can then be adressed by name
in [set_default_proof_mode].
One mode is already registered - the standard mode - named "No",
It corresponds to Coq default setting are they are set when coqtop starts. *)
val register_proof_mode : proof_mode -> unit
val there_is_a_proof : unit -> bool
val there_are_pending_proofs : unit -> bool
val check_no_pending_proof : unit -> unit
val get_current_proof_name : unit -> Names.identifier
val get_all_proof_names : unit -> Names.identifier list
val discard : Names.identifier Util.located -> unit
val discard_current : unit -> unit
val discard_all : unit -> unit
(** [set_proof_mode] sets the proof mode to be used after it's called. It is
typically called by the Proof Mode command. *)
val set_proof_mode : string -> unit
exception NoCurrentProof
val give_me_the_proof : unit -> Proof.proof
(** [start_proof s str goals ~init_tac ~compute_guard hook] starts
a proof of name [s] and
conclusion [t]; [hook] is optionally a function to be applied at
proof end (e.g. to declare the built constructions as a coercion
or a setoid morphism). *)
type lemma_possible_guards = int list list
val start_proof : Names.identifier ->
Decl_kinds.goal_kind ->
(Environ.env * Term.types) list ->
?compute_guard:lemma_possible_guards ->
Tacexpr.declaration_hook ->
unit
val close_proof : unit ->
Names.identifier *
(Entries.definition_entry list *
lemma_possible_guards *
Decl_kinds.goal_kind *
Tacexpr.declaration_hook)
exception NoSuchProof
(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
no current proof. *)
val run_tactic : unit Proofview.tactic -> unit
(** Sets the tactic to be used when a tactic line is closed with [...] *)
val set_endline_tactic : unit Proofview.tactic -> unit
(** Sets the section variables assumed by the proof *)
val set_used_variables : Names.identifier list -> unit
val get_used_variables : unit -> Sign.section_context option
(** Appends the endline tactic of the current proof to a tactic. *)
val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic
(**********************************************************)
(* *)
(* Utility functions *)
(* *)
(**********************************************************)
(** [maximal_unfocus k p] unfocuses [p] until [p] has at least a
focused goal or that the last focus isn't of kind [k]. *)
val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit
(**********************************************************)
(* *)
(* Bullets *)
(* *)
(**********************************************************)
module Bullet : sig
type t = Vernacexpr.bullet
(** A [behavior] is the data of a put function which
is called when a bullet prefixes a tactic, together
with a name to identify it. *)
type behavior = {
name : string;
put : Proof.proof -> t -> unit
}
(** A registered behavior can then be accessed in Coq
through the command [Set Bullet Behavior "name"].
Two modes are registered originally:
* "Strict Subproofs":
- If this bullet follows another one of its kind, defocuses then focuses
(which fails if the focused subproof is not complete).
- If it is the first bullet of its kind, then focuses a new subproof.
* "None": bullets don't do anything *)
val register_behavior : behavior -> unit
(** Handles focusing/defocusing with bullets:
*)
val put : Proof.proof -> t -> unit
end
module V82 : sig
val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook)
end
|
