Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 95 insertions, 0 deletions

diff --git a/library/global.mli b/library/global.mli
new file mode 100644
index 00000000..1da5965c
--- /dev/null
+++ b/library/global.mli
@@ -0,0 +1,95 @@
+(************************************************************************)
+(*  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: global.mli,v 1.40.2.1 2004/07/16 19:30:35 herbelin Exp $ 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 universes : unit -> universes
+val named_context : unit -> Sign.named_context
+
+(*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 -> kernel_name
+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 : Environ.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 -> (mod_bound_id * module_type_entry) list 
+    -> module_type_entry option 
+      -> module_path
+
+val end_module :
+  identifier -> module_path
+
+val start_modtype :
+  identifier -> (mod_bound_id * module_type_entry) list
+    -> 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 : Sign.named_context -> Environ.env
+