Imported Upstream version 8.5~beta1+dfsg

1 files changed, 101 insertions, 64 deletions

diff --git a/library/global.mli b/library/global.mli
index e1cd5c7b..af23d9b7 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -1,106 +1,143 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <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
-open Univ
-open Term
-open Declarations
-open Entries
-open Indtypes
-open Mod_subst
-open Safe_typing
-
-(** This module defines the global environment of Coq.  The functions
+
+(** 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 safe_env : unit -> Safe_typing.safe_environment
 val env : unit -> Environ.env
 
-val env_is_empty : unit -> bool
+val env_is_initial : unit -> bool
 
-val universes : unit -> universes
+val universes : unit -> Univ.universes
 val named_context_val : unit -> Environ.named_context_val
-val named_context : unit -> Sign.named_context
+val named_context : unit -> Context.named_context
 
-val env_is_empty : unit -> bool
+(** {6 Enriching the global environment } *)
 
-(** {6 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
+(** Changing the (im)predicativity of the system *)
+val set_engagement : Declarations.engagement -> unit
+val set_type_in_type : unit -> unit
 
-(** {6 ... } *)
-(** Adding constants, inductives, modules and module types.  All these
-  functions verify that given names match those generated by kernel *)
+(** 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 :
-  dir_path -> identifier -> global_declaration -> constant
-val add_mind        :
-  dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive
-
-val add_module      :
- identifier -> module_entry -> inline -> module_path * delta_resolver
-val add_modtype     :
- identifier -> module_struct_entry -> inline -> module_path
-val add_include :
- module_struct_entry -> bool -> inline -> delta_resolver
+  DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
+val add_mind :
+  DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
 
-val add_constraints : constraints -> unit
+(** Extra universe constraints *)
+val add_constraints : Univ.constraints -> unit
 
-val set_engagement : engagement -> unit
+val push_context : Univ.universe_context -> unit
+val push_context_set : Univ.universe_context_set -> unit
 
-(** {6 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. *)
+(** Non-interactive modules and module types *)
 
-(** [start_*] functions return the [module_path] valid for components
-   of the started module / module type *)
+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
 
-val start_module : identifier -> module_path
+(** Interactive modules and module types *)
 
-val end_module : Summary.frozen ->identifier ->
-  (module_struct_entry * inline) option -> module_path * delta_resolver
+val start_module : Id.t -> module_path
+val start_modtype : Id.t -> module_path
 
-val add_module_parameter :
- mod_bound_id -> module_struct_entry -> inline -> delta_resolver
+val end_module : Summary.frozen -> Id.t ->
+  (Entries.module_struct_entry * Declarations.inline) option ->
+    module_path * MBId.t list * Mod_subst.delta_resolver
 
-val start_modtype : identifier -> module_path
-val end_modtype : Summary.frozen -> identifier -> module_path
-val pack_module : unit -> module_body
+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
 
-(** 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_kn : kernel_name -> constant
 val mind_of_delta_kn : kernel_name -> mutual_inductive
-val exists_objlabel  : label -> bool
 
-(** 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
+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 } *)
 
-(** {6 ... } *)
 (** 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
 
+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
+val type_of_global_unsafe : Globnames.global_reference -> Constr.types 
+
+(** Returns the universe context of the global reference (whatever it's 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
 
-(** spiwack: register/unregister function for retroknowledge *)
-val register : Retroknowledge.field -> constr -> constr -> unit
+val global_env_summary_name : string