blob: e790c39022154a0d5c618e666f7f1eef746c1498 (
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
132
133
134
135
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <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
(** {4 Proofs attached to a constant} *)
type t
(** [Lemmas.t] represents a constant that is being proved, usually
interactively *)
val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
(** [set_endline_tactic tac lemma] set ending tactic for [lemma] *)
val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t
(** [pf_map f l] map the underlying proof object *)
val pf_fold : (Proof_global.t -> 'a) -> t -> 'a
(** [pf_fold f l] fold over the underlying proof object *)
val by : unit Proofview.tactic -> t -> t * bool
(** [by tac l] apply a tactic to [l] *)
(** Creating high-level proofs with an associated constant *)
module Proof_ending : sig
type t =
| Regular
| End_obligation of DeclareObl.obligation_qed_info
| End_derive of { f : Id.t; name : Id.t }
| End_equations of { hook : Constant.t list -> Evd.evar_map -> unit
; i : Id.t
; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
; wits : EConstr.t list ref
; sigma : Evd.evar_map
}
end
module Recthm : sig
type t =
{ name : Id.t
(** Name of theorem *)
; typ : EConstr.t
(** Type of theorem *)
; args : Name.t list
(** Names to pre-introduce *)
; impargs : Impargs.manual_implicits
(** Explicitily declared implicit arguments *)
}
end
module Info : sig
type t
val make
: ?hook: DeclareDef.Hook.t
(** Callback to be executed at the end of the proof *)
-> ?proof_ending : Proof_ending.t
(** Info for special constants *)
-> ?scope : DeclareDef.locality
(** locality *)
-> ?kind:Decls.logical_kind
(** Theorem, etc... *)
-> unit
-> t
end
(** Starts the proof of a constant *)
val start_lemma
: name:Id.t
-> poly:bool
-> ?udecl:UState.universe_decl
-> ?info:Info.t
-> Evd.evar_map
-> EConstr.types
-> t
val start_dependent_lemma
: name:Id.t
-> poly:bool
-> ?udecl:UState.universe_decl
-> ?info:Info.t
-> Proofview.telescope
-> t
type lemma_possible_guards = int list list
(** Pretty much internal, only used in ComFixpoint *)
val start_lemma_with_initialization
: ?hook:DeclareDef.Hook.t
-> poly:bool
-> scope:DeclareDef.locality
-> kind:Decls.logical_kind
-> udecl:UState.universe_decl
-> Evd.evar_map
-> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
-> Recthm.t list
-> int list option
-> t
val default_thm_id : Names.Id.t
(** {4 Saving proofs} *)
val save_lemma_admitted : lemma:t -> unit
val save_lemma_proved
: lemma:t
-> opaque:Proof_global.opacity_flag
-> idopt:Names.lident option
-> unit
(** To be removed, don't use! *)
module Internal : sig
val get_info : t -> Info.t
(** Only needed due to the Proof_global compatibility layer. *)
end
(** Special cases for delayed proofs, in this case we must provide the
proof information so the proof won't be forced. *)
val save_lemma_admitted_delayed : proof:Proof_global.proof_object -> info:Info.t -> unit
val save_lemma_proved_delayed
: proof:Proof_global.proof_object
-> info:Info.t
-> idopt:Names.lident option
-> unit
|
