blob: bd2e87ac3accbafa51217e5f73ada22d2ac5c74f (
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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 : (Declare.Proof.t -> Declare.Proof.t) -> t -> t
(** [pf_map f l] map the underlying proof object *)
val pf_fold : (Declare.Proof.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
; sigma : Evd.evar_map
}
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
-> ?impargs:Impargs.manual_implicits
-> 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, used by the Lemma / Fixpoint vernaculars *)
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 * Constr.t option list option) option
-> DeclareDef.Recthm.t list
-> int list option
-> t
(** {4 Saving proofs} *)
val save_lemma_admitted : lemma:t -> unit
val save_lemma_proved
: lemma:t
-> opaque:Declare.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 Declare 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:Declare.proof_object -> info:Info.t -> unit
val save_lemma_proved_delayed
: proof:Declare.proof_object
-> info:Info.t
-> idopt:Names.lident option
-> unit
|
