From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 kernel/safe_typing.mli | 51 +++++++++++++++++++++++++-------------------------
 1 file changed, 25 insertions(+), 26 deletions(-)

(limited to 'kernel/safe_typing.mli')

diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6d656f8b..c378d8cc 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -6,13 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: safe_typing.mli 10664 2008-03-14 11:27:37Z soubiran $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
 open Term
 open Declarations
 open Entries
+open Mod_subst
 (*i*)
 
 (*s Safe environments. Since we are now able to type terms, we can
@@ -20,7 +21,7 @@ open Entries
   typed before being added.
 
   We also add [open_structure] and [close_section], [close_module] to
-  provide functionnality for sections and interactive modules 
+  provide functionnality for sections and interactive modules
 *)
 
 type safe_environment
@@ -39,35 +40,31 @@ val push_named_def :
     Univ.constraints * safe_environment
 
 (* Adding global axioms or definitions *)
-type global_declaration = 
+type global_declaration =
   | ConstantEntry of constant_entry
   | GlobalRecipe of Cooking.recipe
 
-val add_constant : 
-  dir_path -> label -> global_declaration -> safe_environment -> 
+val add_constant :
+  dir_path -> label -> global_declaration -> safe_environment ->
       constant * safe_environment
 
 (* Adding an inductive type *)
-val add_mind : 
+val add_mind :
   dir_path -> label -> mutual_inductive_entry -> safe_environment ->
     mutual_inductive * safe_environment
 
 (* Adding a module *)
 val add_module :
-  label -> module_entry -> safe_environment 
-    -> module_path * safe_environment
+  label -> module_entry -> bool -> safe_environment
+    -> module_path * delta_resolver * safe_environment
 
-(* Adding a module alias*)
-val add_alias :
-  label -> module_path -> safe_environment 
-    -> module_path * safe_environment
 (* Adding a module type *)
 val add_modtype :
-  label -> module_struct_entry -> safe_environment 
+  label -> module_struct_entry -> bool -> safe_environment
     -> module_path * safe_environment
 
 (* Adding universe constraints *)
-val add_constraints : 
+val add_constraints :
   Univ.constraints -> safe_environment -> safe_environment
 
 (* Settin the strongly constructive or classical logical engagement *)
@@ -75,14 +72,15 @@ val set_engagement : engagement -> safe_environment -> safe_environment
 
 
 (*s Interactive module functions *)
-val start_module : 
+val start_module :
   label -> safe_environment -> module_path * safe_environment
+
 val end_module :
-  label -> module_struct_entry option 
-      -> safe_environment -> module_path * safe_environment 
+  label -> (module_struct_entry * bool) option
+      -> safe_environment -> module_path * delta_resolver * safe_environment 
 
 val add_module_parameter :
-  mod_bound_id -> module_struct_entry -> safe_environment -> safe_environment
+  mod_bound_id -> module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment
 
 val start_modtype :
   label -> safe_environment -> module_path * safe_environment
@@ -91,24 +89,25 @@ val end_modtype :
   label -> safe_environment -> module_path * safe_environment
 
 val add_include :
-  module_struct_entry -> safe_environment -> safe_environment
+  module_struct_entry -> bool -> bool -> safe_environment ->
+   delta_resolver * safe_environment
 
+val pack_module : safe_environment -> module_body
 val current_modpath : safe_environment -> module_path
-val current_msid : safe_environment -> mod_self_id
-
-
+val delta_of_senv : safe_environment -> delta_resolver*delta_resolver
+  
 (* Loading and saving compilation units *)
 
 (* exporting and importing modules *)
 type compiled_library
 
-val start_library : dir_path -> safe_environment 
+val start_library : dir_path -> safe_environment
       -> module_path * safe_environment
 
-val export : safe_environment -> dir_path  
-      -> mod_self_id * compiled_library
+val export : safe_environment -> dir_path
+      -> module_path * compiled_library
 
-val import : compiled_library -> Digest.t -> safe_environment 
+val import : compiled_library -> Digest.t -> safe_environment
       -> module_path * safe_environment
 
 (* Remove the body of opaque constants *)
-- 
cgit v1.2.3