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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <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) *)
(************************************************************************)
open Names
open Decl_kinds
(* Declaration hooks *)
type declaration_hook
(* Hooks allow users of the API to perform arbitrary actions at
* proof/definition saving time. For example, to register a constant
* as a Coercion, perform some cleanup, update the search database,
* etc...
*
* Here, we use an extended hook type suitable for obligations /
* equations.
*)
(** [hook_type] passes to the client:
- [ustate]: universe constraints obtained when the term was closed
- [(n1,t1),...(nm,tm)]: association list between obligation
name and the corresponding defined term (might be a constant,
but also an arbitrary term in the Expand case of obligations)
- [locality]: Locality of the original declaration
- [ref]: identifier of the origianl declaration
*)
type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
val mk_hook : hook_type -> declaration_hook
val call_hook
: ?hook:declaration_hook
-> ?fix_exn:Future.fix_exn
-> hook_type
(* Proofs that define a constant + terminators *)
type t
type proof_terminator
type lemma_possible_guards = int list list
module Stack : sig
type lemma = t
type t
val pop : t -> lemma * t option
val push : t option -> lemma -> t
val map_top : f:(lemma -> lemma) -> t -> t
val map_top_pstate : f:(Proof_global.t -> Proof_global.t) -> t -> t
val with_top : t -> f:(lemma -> 'a ) -> 'a
val with_top_pstate : t -> f:(Proof_global.t -> 'a ) -> 'a
val get_all_proof_names : t -> Names.Id.t list
val copy_info : src:t -> tgt:t -> t
(** Gets the current info without checking that the proof has been
completed. Useful for the likes of [Admitted]. *)
end
val standard_proof_terminator : proof_terminator
val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t
val pf_fold : (Proof_global.t -> 'a) -> t -> 'a
val by : unit Proofview.tactic -> t -> t * bool
(* Start of high-level proofs with an associated constant *)
val start_lemma
: Id.t
-> ?pl:UState.universe_decl
-> goal_kind
-> Evd.evar_map
-> ?terminator:proof_terminator
-> ?sign:Environ.named_context_val
-> ?compute_guard:lemma_possible_guards
-> ?hook:declaration_hook
-> EConstr.types
-> t
val start_dependent_lemma
: Id.t
-> ?pl:UState.universe_decl
-> goal_kind
-> ?terminator:proof_terminator
-> ?sign:Environ.named_context_val
-> ?compute_guard:lemma_possible_guards
-> ?hook:declaration_hook
-> Proofview.telescope
-> t
val start_lemma_com
: program_mode:bool
-> ?inference_hook:Pretyping.inference_hook
-> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
-> t
val start_lemma_with_initialization
: ?hook:declaration_hook
-> goal_kind -> Evd.evar_map -> UState.universe_decl
-> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
-> (Id.t (* name of thm *) *
(EConstr.types (* type of thm *) *
(Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list
-> int list option
-> t
val default_thm_id : Names.Id.t
(* Prepare global named context for proof session: remove proofs of
opaque section definitions and remove vm-compiled code *)
val initialize_named_context_for_proof : unit -> Environ.named_context_val
(** {6 Saving proofs } *)
type proof_info
val default_info : proof_info
val save_lemma_admitted
: ?proof:(Proof_global.proof_object * proof_info)
-> lemma:t
-> unit
val save_lemma_proved
: ?proof:(Proof_global.proof_object * proof_info)
-> ?lemma:t
-> opaque:Proof_global.opacity_flag
-> idopt:Names.lident option
-> unit
(* API to build a terminator, should go away *)
type proof_ending =
| Admitted of
Names.Id.t *
Decl_kinds.goal_kind *
Entries.parameter_entry *
UState.t *
declaration_hook option
| Proved of
Proof_global.opacity_flag *
lident option *
Proof_global.proof_object *
declaration_hook option *
lemma_possible_guards
(** This stuff is internal and will be removed in the future. *)
module Internal : sig
(** Only needed due to the Proof_global compatibility layer. *)
val get_info : t -> proof_info
(** Only needed by obligations, should be reified soon *)
val make_terminator : (proof_ending -> unit) -> proof_terminator
val apply_terminator : proof_terminator -> proof_ending -> unit
end
|
