blob: 17f5c73560662b70f965ea938ae82226cf2cfe40 (
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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(** This module defines proof facilities relevant to the
toplevel. In particular it defines the global proof
environment. *)
type t
(* Should be moved into a proper view *)
val get_proof : t -> Proof.t
val get_proof_name : t -> Names.Id.t
val get_persistence : t -> Decl_kinds.goal_kind
val get_used_variables : t -> Constr.named_context option
(** Get the universe declaration associated to the current proof. *)
val get_universe_decl : t -> UState.universe_decl
val compact_the_proof : t -> t
(** When a proof is closed, it is reified into a [proof_object], where
[id] is the name of the proof, [entries] the list of the proof terms
(in a form suitable for definitions). Together with the [terminator]
function which takes a [proof_object] together with a [proof_end]
(i.e. an proof ending command) and registers the appropriate
values. *)
type 'a proof_entry = {
proof_entry_body : 'a Entries.const_entry_body;
(* List of section variables *)
proof_entry_secctx : Constr.named_context option;
(* State id on which the completion of type checking is reported *)
proof_entry_feedback : Stateid.t option;
proof_entry_type : Constr.types option;
proof_entry_universes : Entries.universes_entry;
proof_entry_opaque : bool;
proof_entry_inline_code : bool;
}
type proof_object = {
id : Names.Id.t;
entries : Evd.side_effects proof_entry list;
persistence : Decl_kinds.goal_kind;
universes: UState.t;
}
type opacity_flag = Opaque | Transparent
(** [start_proof id str pl goals] starts a proof of name
[id] with goals [goals] (a list of pairs of environment and
conclusion); [str] describes what kind of theorem/definition this
is; [terminator] is used at the end of the proof to close the proof
(e.g. to declare the built constructions as a coercion or a setoid
morphism). The proof is started in the evar map [sigma] (which can
typically contain universe constraints), and with universe bindings
pl. *)
val start_proof
: Evd.evar_map
-> Names.Id.t
-> UState.universe_decl
-> Decl_kinds.goal_kind
-> (Environ.env * EConstr.types) list
-> t
(** Like [start_proof] except that there may be dependencies between
initial goals. *)
val start_dependent_proof
: Names.Id.t
-> UState.universe_decl
-> Decl_kinds.goal_kind
-> Proofview.telescope
-> t
(** Update the proofs global environment after a side-effecting command
(e.g. a sublemma definition) has been run inside it. Assumes
there_are_pending_proofs. *)
val update_global_env : t -> t
(* Takes a function to add to the exceptions data relative to the
state in which the proof was built *)
val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object
(* Intermediate step necessary to delegate the future.
* Both access the current proof state. The former is supposed to be
* chained with a computation that completed the proof *)
type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
(* If allow_partial is set (default no) then an incomplete proof
* is allowed (no error), and a warn is given if the proof is complete. *)
val return_proof : ?allow_partial:bool -> t -> closed_proof_output
val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
closed_proof_output Future.computation -> proof_object
val get_open_goals : t -> int
val map_proof : (Proof.t -> Proof.t) -> t -> t
val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
(** Sets the tactic to be used when a tactic line is closed with [...] *)
val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
(** Sets the section variables assumed by the proof, returns its closure
* (w.r.t. type dependencies and let-ins covered by it) + a list of
* ids to be cleared *)
val set_used_variables : t ->
Names.Id.t list -> (Constr.named_context * Names.lident list) * t
|
