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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
(** This module defines the global environment of Coq. The functions
below are exactly the same as the ones in [Safe_typing], operating on
that global environment. [add_*] functions perform name verification,
i.e. check that the name given as argument match those provided by
[Safe_typing]. *)
val safe_env : unit -> Safe_typing.safe_environment
val env : unit -> Environ.env
val env_is_initial : unit -> bool
val universes : unit -> Univ.universes
val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Context.named_context
(** {6 Enriching the global environment } *)
(** Changing the (im)predicativity of the system *)
val set_engagement : Declarations.engagement -> unit
val set_type_in_type : unit -> unit
(** Variables, Local definitions, constants, inductive types *)
val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit
val push_named_def : (Id.t * Entries.definition_entry) -> unit
val add_constant :
DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
val add_mind :
DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
(** Extra universe constraints *)
val add_constraints : Univ.constraints -> unit
val push_context : Univ.universe_context -> unit
val push_context_set : Univ.universe_context_set -> unit
(** Non-interactive modules and module types *)
val add_module :
Id.t -> Entries.module_entry -> Declarations.inline ->
module_path * Mod_subst.delta_resolver
val add_modtype :
Id.t -> Entries.module_type_entry -> Declarations.inline -> module_path
val add_include :
Entries.module_struct_entry -> bool -> Declarations.inline ->
Mod_subst.delta_resolver
(** Interactive modules and module types *)
val start_module : Id.t -> module_path
val start_modtype : Id.t -> module_path
val end_module : Summary.frozen -> Id.t ->
(Entries.module_struct_entry * Declarations.inline) option ->
module_path * MBId.t list * Mod_subst.delta_resolver
val end_modtype : Summary.frozen -> Id.t -> module_path * MBId.t list
val add_module_parameter :
MBId.t -> Entries.module_struct_entry -> Declarations.inline ->
Mod_subst.delta_resolver
(** {6 Queries in the global environment } *)
val lookup_named : variable -> Context.named_declaration
val lookup_constant : constant -> Declarations.constant_body
val lookup_inductive : inductive ->
Declarations.mutual_inductive_body * Declarations.one_inductive_body
val lookup_pinductive : Constr.pinductive ->
Declarations.mutual_inductive_body * Declarations.one_inductive_body
val lookup_mind : mutual_inductive -> Declarations.mutual_inductive_body
val lookup_module : module_path -> Declarations.module_body
val lookup_modtype : module_path -> Declarations.module_type_body
val exists_objlabel : Label.t -> bool
val constant_of_delta_kn : kernel_name -> constant
val mind_of_delta_kn : kernel_name -> mutual_inductive
val opaque_tables : unit -> Opaqueproof.opaquetab
val body_of_constant : constant -> Term.constr option
val body_of_constant_body : Declarations.constant_body -> Term.constr option
val constraints_of_constant_body :
Declarations.constant_body -> Univ.constraints
val universes_of_constant_body :
Declarations.constant_body -> Univ.universe_context
(** {6 Compiled libraries } *)
val start_library : DirPath.t -> module_path
val export : ?except:Future.UUIDSet.t -> DirPath.t ->
module_path * Safe_typing.compiled_library * Safe_typing.native_library
val import :
Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
module_path * Nativecode.symbol array
(** {6 Misc } *)
(** Function to get an environment from the constants part of the global
* environment and a given context. *)
val env_of_context : Environ.named_context_val -> Environ.env
val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
val is_polymorphic : Globnames.global_reference -> bool
val is_template_polymorphic : Globnames.global_reference -> bool
val type_of_global_in_context : Environ.env ->
Globnames.global_reference -> Constr.types Univ.in_universe_context
(** Returns the type of the constant in its global or local universe
context. The type should not be used without pushing it's universe
context in the environmnent of usage. For non-universe-polymorphic
constants, it does not matter. *)
val type_of_global_unsafe : Globnames.global_reference -> Constr.types
(** Returns the type of the constant, forgetting its universe context if
it is polymorphic, use with care: for polymorphic constants, the
type cannot be used to produce a term used by the kernel. For safe
handling of polymorphic global references, one should look at a
particular instantiation of the reference, in some particular
universe context (part of an [env] or [evar_map]), see
e.g. [type_of_constant_in]. If you want to create a fresh instance
of the reference and get its type look at [Evd.fresh_global] or
[Evarutil.new_global] and [Retyping.get_type_of]. *)
(** Returns the universe context of the global reference (whatever its polymorphic status is). *)
val universes_of_global : Globnames.global_reference -> Univ.universe_context
(** {6 Retroknowledge } *)
val register :
Retroknowledge.field -> Term.constr -> Term.constr -> unit
val register_inline : constant -> unit
(** {6 Oracle } *)
val set_strategy : Names.constant Names.tableKey -> Conv_oracle.level -> unit
(* Modifies the global state, registering new universes *)
val current_dirpath : unit -> Names.dir_path
val with_global : (Environ.env -> Names.dir_path -> 'a Univ.in_universe_context_set) -> 'a
val global_env_summary_name : string
|
