From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 kernel/modops.mli | 53 +++++++++++++++++++++++++++--------------------------
 1 file changed, 27 insertions(+), 26 deletions(-)

(limited to 'kernel/modops.mli')

diff --git a/kernel/modops.mli b/kernel/modops.mli
index 61761bb7..2d8b21ad 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.mli 9980 2007-07-12 13:32:37Z soubiran $ i*)
+(*i $Id: modops.mli 10664 2008-03-14 11:27:37Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -20,35 +20,36 @@ open Mod_subst
 
 (* Various operations on modules and module types *)
 
-exception Circularity of string
-exception Not_equiv_path
-
-(* recursively unfold MTBdent module types *)
-val scrape_modtype : env -> module_type_body -> module_type_body
-
 (* make the environment entry out of type *)
 val module_body_of_type : module_type_body -> module_body
 
-val module_body_of_spec : module_specification_body -> module_body 
-
-val module_spec_of_body : module_body -> module_specification_body
-
+val  module_type_of_module : module_path option -> module_body -> 
+  module_type_body 
 
 val destr_functor : 
-  module_type_body -> mod_bound_id * module_type_body * module_type_body
-
+  env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body
 
 val subst_modtype : substitution -> module_type_body -> module_type_body
+val subst_structure : substitution -> structure_body -> structure_body
+
+val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
 
 val subst_signature_msid :
   mod_self_id -> module_path -> 
-  module_signature_body -> module_signature_body
+  structure_body -> structure_body
+
+val subst_structure : substitution -> structure_body -> structure_body
+
+(* Evaluation functions *)
+val eval_struct : env -> struct_expr_body -> struct_expr_body
+
+val type_of_mb : env -> module_body -> struct_expr_body
 
 (* [add_signature mp sign env] assumes that the substitution [msid]
    $\mapsto$ [mp] has already been performed (or is not necessary, like
    when [mp = MPself msid]) *)
 val add_signature : 
-  module_path -> module_signature_body -> env -> env
+  module_path -> structure_body -> env -> env
 
 (* adds a module and its components, but not the constraints *)
 val add_module :
@@ -56,22 +57,24 @@ val add_module :
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
-val strengthen : env -> module_type_body -> module_path -> module_type_body
+val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body
+
+val update_subst : env -> module_body -> module_path -> bool * substitution
 
 val error_existing_label : label -> 'a
 
-val error_declaration_not_path : module_expr -> 'a
+val error_declaration_not_path : module_struct_entry -> 'a
 
-val error_application_to_not_path : module_expr -> 'a
+val error_application_to_not_path : module_struct_entry -> 'a
 
-val error_not_a_functor : module_expr -> 'a
+val error_not_a_functor :  module_struct_entry -> 'a
 
 val error_incompatible_modtypes : 
   module_type_body -> module_type_body -> 'a
 
 val error_not_equal : module_path -> module_path -> 'a
 
-val error_not_match : label -> string -> string -> 'a
+val error_not_match : label -> structure_field_body -> 'a
   
 val error_incompatible_labels : label -> label -> 'a
 
@@ -79,7 +82,7 @@ val error_no_such_label : label -> 'a
 
 val error_result_must_be_signature : unit -> 'a
 
-val error_signature_expected : module_type_body -> 'a
+val error_signature_expected : struct_expr_body -> 'a
 
 val error_no_module_to_end : unit -> 'a 
 
@@ -99,11 +102,9 @@ val error_a_generative_module_expected : label -> 'a
 
 val error_local_context : label option -> 'a
 
-val error_circular_with_module : identifier -> 'a
-
-val error_circularity_in_subtyping : string->string->string-> 'a
-
 val error_no_such_label_sub : label->string->string->'a
 
 val resolver_of_environment :
- mod_bound_id -> module_type_body -> module_path -> env -> resolver
+  mod_bound_id -> module_type_body -> module_path -> substitution 
+  -> env -> resolver
+
-- 
cgit v1.2.3