blob: 5675cf681103f9f2ddc9ce2e01a15905dd381113 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \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 Mod_subst
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 -> mutual_inductive
val add_module :
identifier -> module_entry -> bool -> module_path * delta_resolver
val add_modtype :
identifier -> module_struct_entry -> bool -> module_path
val add_include :
module_struct_entry -> bool -> bool -> delta_resolver
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 : Summary.frozen ->identifier ->
(module_struct_entry * bool) option -> module_path * delta_resolver
val add_module_parameter :
mod_bound_id -> module_struct_entry -> bool -> delta_resolver
val start_modtype : identifier -> module_path
val end_modtype : Summary.frozen -> identifier -> module_path
val pack_module : unit -> module_body
(* 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 : module_path -> module_type_body
val constant_of_delta : constant -> constant
val mind_of_delta : mutual_inductive -> mutual_inductive
(* Compiled modules *)
val start_library : dir_path -> module_path
val export : dir_path -> module_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
(* spiwack: register/unregister function for retroknowledge *)
val register : Retroknowledge.field -> constr -> constr -> unit
|
