blob: c646d2f85b58231a452baccff92a72bbe0e145c3 (
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
136
137
138
139
140
141
142
143
144
145
146
147
148
|
(************************************************************************)
(* * 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
open Constr
open Entries
(** This module provides the official functions to declare new variables,
parameters, constants and inductive types. Using the following functions
will add the entries in the global environment (module [Global]), will
register the declarations in the library (module [Lib]) --- so that the
reset works properly --- and will fill some global tables such as
[Nametab] and [Impargs]. *)
(** Proof entries *)
type 'a proof_entry = private {
proof_entry_body : 'a Entries.const_entry_body;
(* List of section variables *)
proof_entry_secctx : Id.Set.t 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;
}
(** Declaration of local constructions (Variable/Hypothesis/Local) *)
type variable_declaration =
| SectionLocalDef of Evd.side_effects proof_entry
| SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
type 'a constant_entry =
| DefinitionEntry of 'a proof_entry
| ParameterEntry of parameter_entry
| PrimitiveEntry of primitive_entry
val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
val declare_variable
: name:variable
-> kind:Decls.logical_kind
-> variable_declaration
-> unit
(** Declaration of global constructions
i.e. Definition/Theorem/Axiom/Parameter/... *)
(* Default definition entries, transparent with no secctx or proj information *)
val definition_entry
: ?fix_exn:Future.fix_exn
-> ?opaque:bool
-> ?inline:bool
-> ?types:types
-> ?univs:Entries.universes_entry
-> ?eff:Evd.side_effects
-> constr
-> Evd.side_effects proof_entry
val pure_definition_entry
: ?fix_exn:Future.fix_exn
-> ?opaque:bool
-> ?inline:bool
-> ?types:types
-> ?univs:Entries.universes_entry
-> constr
-> unit proof_entry
(* Delayed definition entries *)
val delayed_definition_entry
: ?opaque:bool
-> ?inline:bool
-> ?feedback_id:Stateid.t
-> ?section_vars:Id.Set.t
-> ?univs:Entries.universes_entry
-> ?types:types
-> 'a Entries.const_entry_body
-> 'a proof_entry
type import_status = ImportDefaultBehavior | ImportNeedQualified
(** [declare_constant id cd] declares a global declaration
(constant/parameter) with name [id] in the current section; it returns
the full path of the declaration
internal specify if the constant has been created by the kernel or by the
user, and in the former case, if its errors should be silent *)
val declare_constant
: ?local:import_status
-> name:Id.t
-> kind:Decls.logical_kind
-> Evd.side_effects constant_entry
-> Constant.t
val declare_private_constant
: ?role:Evd.side_effect_role
-> ?local:import_status
-> name:Id.t
-> kind:Decls.logical_kind
-> unit proof_entry
-> Constant.t * Evd.side_effects
(** [inline_private_constants ~sideff ~univs env ce] will inline the
constants in [ce]'s body and return the body plus the updated
[UState.t]. *)
val inline_private_constants
: univs:UState.t
-> Environ.env
-> Evd.side_effects proof_entry
-> Constr.t * UState.t
(** Declaration messages *)
val definition_message : Id.t -> unit
val assumption_message : Id.t -> unit
val fixpoint_message : int array option -> Id.t list -> unit
val cofixpoint_message : Id.t list -> unit
val recursive_message : bool (** true = fixpoint *) ->
int array option -> Id.t list -> unit
val check_exists : Id.t -> unit
(* Used outside this module only in indschemes *)
exception AlreadyDeclared of (string option * Id.t)
(* For legacy support, do not use *)
module Internal : sig
val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry
(* Overriding opacity is indeed really hacky *)
val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry
(* TODO: This is only used in DeclareDef to forward the fix to
hooks, should eventually go away *)
val get_fix_exn : 'a proof_entry -> Future.fix_exn
val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
end
|
