1 files changed, 170 insertions, 0 deletions
diff --git a/library/global.mli b/library/global.mli
new file mode 100644
index 0000000000..ca88d2dafd
--- /dev/null
+++ b/library/global.mli
@@ -0,0 +1,170 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <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
+
+(** 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 -> UGraph.t
+val named_context_val : unit -> Environ.named_context_val
+val named_context : unit -> Constr.named_context
+
+(** {6 Enriching the global environment } *)
+
+(** Changing the (im)predicativity of the system *)
+val set_engagement : Declarations.engagement -> unit
+val set_indices_matter : bool -> unit
+val set_typing_flags : Declarations.typing_flags -> unit
+val typing_flags : unit -> Declarations.typing_flags
+val make_sprop_cumulative : unit -> unit
+val set_allow_sprop : bool -> unit
+val sprop_allowed : unit -> bool
+
+(** Variables, Local definitions, constants, inductive types *)
+
+val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
+val push_named_def   : (Id.t * Entries.section_def_entry) -> unit
+
+val export_private_constants : in_section:bool ->
+  Safe_typing.private_constants Entries.definition_entry ->
+  unit Entries.definition_entry * Safe_typing.exported_private_constant list
+
+val add_constant :
+  in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t
+val add_mind :
+  Id.t -> Entries.mutual_inductive_entry -> MutInd.t
+
+(** Extra universe constraints *)
+val add_constraints : Univ.Constraint.t -> unit
+
+val push_context_set : bool -> Univ.ContextSet.t -> unit
+
+(** Non-interactive modules and module types *)
+
+val add_module :
+  Id.t -> Entries.module_entry -> Declarations.inline ->
+    ModPath.t * Mod_subst.delta_resolver
+val add_modtype :
+  Id.t -> Entries.module_type_entry -> Declarations.inline -> ModPath.t
+val add_include :
+  Entries.module_struct_entry -> bool -> Declarations.inline ->
+    Mod_subst.delta_resolver
+
+(** Interactive modules and module types *)
+
+val start_module : Id.t -> ModPath.t
+val start_modtype : Id.t -> ModPath.t
+
+val end_module : Summary.frozen -> Id.t ->
+  (Entries.module_struct_entry * Declarations.inline) option ->
+    ModPath.t * MBId.t list * Mod_subst.delta_resolver
+
+val end_modtype : Summary.frozen -> Id.t -> ModPath.t * 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 -> Constr.named_declaration
+val lookup_constant  : Constant.t -> 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      : MutInd.t -> Declarations.mutual_inductive_body
+val lookup_module    : ModPath.t -> Declarations.module_body
+val lookup_modtype   : ModPath.t -> Declarations.module_type_body
+val exists_objlabel  : Label.t -> bool
+
+val constant_of_delta_kn : KerName.t -> Constant.t
+val mind_of_delta_kn : KerName.t -> MutInd.t
+
+val opaque_tables : unit -> Opaqueproof.opaquetab
+
+val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option
+(** Returns the body of the constant if it has any, and the polymorphic context
+    it lives in. For monomorphic constant, the latter is empty, and for
+    polymorphic constants, the term contains De Bruijn universe variables that
+    need to be instantiated. *)
+
+val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
+
+(** {6 Compiled libraries } *)
+
+val start_library : DirPath.t -> ModPath.t
+val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t ->
+  ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library
+val import :
+  Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest ->
+  ModPath.t
+
+(** {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_joined_environment : unit -> bool
+
+val is_polymorphic : GlobRef.t -> bool
+val is_template_polymorphic : GlobRef.t -> bool
+val is_type_in_type : GlobRef.t -> bool
+
+val constr_of_global_in_context : Environ.env ->
+  GlobRef.t -> Constr.types * Univ.AUContext.t
+  [@@ocaml.deprecated "alias of [Typeops.constr_of_global_in_context]"]
+
+val type_of_global_in_context : Environ.env -> 
+  GlobRef.t -> Constr.types * Univ.AUContext.t
+  [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"]
+
+(** Returns the universe context of the global reference (whatever its polymorphic status is). *)
+val universes_of_global : GlobRef.t -> Univ.AUContext.t
+[@@ocaml.deprecated "Use [Environ.universes_of_global]"]
+
+(** {6 Retroknowledge } *)
+
+val register_inline : Constant.t -> unit
+val register_inductive : inductive -> CPrimitives.prim_ind -> unit
+
+(** {6 Oracle } *)
+
+val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
+
+(** {6 Conversion settings } *)
+
+val set_share_reduction : bool -> unit
+
+val set_VM : bool -> unit
+val set_native_compiler : bool -> unit
+
+(* Modifies the global state, registering new universes *)
+
+val current_modpath : unit -> ModPath.t
+
+val current_dirpath : unit -> DirPath.t
+
+val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a
+
+val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag