blob: 6842a44eb85f22139212d639f4069450a3fd46b8 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Names
open Univ
open Term
open Declarations
open Entries
open Indtypes
open Safe_typing
(*i*)
(* 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_environment
val env : unit -> Environ.env
val env_is_empty : unit -> bool
val universes : unit -> universes
val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Sign.named_context
val env_is_empty : unit -> bool
(*s Extending env with variables and local definitions *)
val push_named_assum : (identifier * types) -> Univ.constraints
val push_named_def : (identifier * constr * types option) -> Univ.constraints
(*s Adding constants, inductives, modules and module types. All these
functions verify that given names match those generated by kernel *)
val add_constant :
dir_path -> identifier -> global_declaration -> constant
val add_mind :
dir_path -> identifier -> mutual_inductive_entry -> kernel_name
val add_module : identifier -> module_entry -> module_path
val add_modtype : identifier -> module_type_entry -> kernel_name
val add_constraints : constraints -> unit
val set_engagement : engagement -> unit
(*s Interactive modules and module types *)
(* Both [start_*] functions take the [dir_path] argument to create a
[mod_self_id]. This should be the name of the compilation unit. *)
(* [start_*] functions return the [module_path] valid for components
of the started module / module type *)
val start_module : identifier -> module_path
val end_module : identifier -> module_type_entry option -> module_path
val add_module_parameter : mod_bound_id -> module_type_entry -> unit
val start_modtype : identifier -> module_path
val end_modtype : identifier -> kernel_name
(* Queries *)
val lookup_named : variable -> named_declaration
val lookup_constant : constant -> constant_body
val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
val lookup_mind : mutual_inductive -> mutual_inductive_body
val lookup_module : module_path -> module_body
val lookup_modtype : kernel_name -> module_type_body
(* Compiled modules *)
val start_library : dir_path -> module_path
val export : dir_path -> compiled_library
val import : compiled_library -> Digest.t -> module_path
(*s Function to get an environment from the constants part of the global
* environment and a given context. *)
val type_of_global : Libnames.global_reference -> types
val env_of_context : Environ.named_context_val -> Environ.env
|
