1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: global.mli 10664 2008-03-14 11:27:37Z soubiran $ i*)
21
(* This module defines the global environment of Coq. The functions
22
below are exactly the same as the ones in [Safe_typing], operating on
23
that global environment. [add_*] functions perform name verification,
24
i.e. check that the name given as argument match those provided by
29
val safe_env : unit -> safe_environment
30
val env : unit -> Environ.env
32
val env_is_empty : unit -> bool
34
val universes : unit -> universes
35
val named_context_val : unit -> Environ.named_context_val
36
val named_context : unit -> Sign.named_context
38
val env_is_empty : unit -> bool
40
(*s Extending env with variables and local definitions *)
41
val push_named_assum : (identifier * types) -> Univ.constraints
42
val push_named_def : (identifier * constr * types option) -> Univ.constraints
44
(*s Adding constants, inductives, modules and module types. All these
45
functions verify that given names match those generated by kernel *)
48
dir_path -> identifier -> global_declaration -> constant
50
dir_path -> identifier -> mutual_inductive_entry -> kernel_name
52
val add_module : identifier -> module_entry -> module_path
53
val add_modtype : identifier -> module_struct_entry -> module_path
54
val add_include : module_struct_entry -> unit
55
val add_alias : identifier -> module_path -> module_path
57
val add_constraints : constraints -> unit
59
val set_engagement : engagement -> unit
61
(*s Interactive modules and module types *)
62
(* Both [start_*] functions take the [dir_path] argument to create a
63
[mod_self_id]. This should be the name of the compilation unit. *)
65
(* [start_*] functions return the [module_path] valid for components
66
of the started module / module type *)
68
val start_module : identifier -> module_path
69
val end_module : identifier -> module_struct_entry option -> module_path
71
val add_module_parameter : mod_bound_id -> module_struct_entry -> unit
73
val start_modtype : identifier -> module_path
74
val end_modtype : identifier -> module_path
79
val lookup_named : variable -> named_declaration
80
val lookup_constant : constant -> constant_body
81
val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
82
val lookup_mind : mutual_inductive -> mutual_inductive_body
83
val lookup_module : module_path -> module_body
84
val lookup_modtype : module_path -> module_type_body
86
(* Compiled modules *)
87
val start_library : dir_path -> module_path
88
val export : dir_path -> compiled_library
89
val import : compiled_library -> Digest.t -> module_path
91
(*s Function to get an environment from the constants part of the global
92
* environment and a given context. *)
94
val type_of_global : Libnames.global_reference -> types
95
val env_of_context : Environ.named_context_val -> Environ.env
98
(* spiwack: register/unregister function for retroknowledge *)
99
val register : Retroknowledge.field -> constr -> constr -> unit