From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 kernel/mod_typing.mli | 53 +++++++++++++++++++++++----------------------------
 1 file changed, 24 insertions(+), 29 deletions(-)

(limited to 'kernel/mod_typing.mli')

diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index e868aec2..b39e8212 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  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        *)
@@ -12,40 +12,35 @@ open Entries
 open Mod_subst
 open Names
 
+(** Main functions for translating module entries *)
 
 val translate_module :
   env -> module_path -> inline -> module_entry -> module_body
 
-val translate_module_type :
-  env -> module_path -> inline -> module_struct_entry -> module_type_body
+val translate_modtype :
+  env -> module_path -> inline -> module_type_entry -> module_type_body
 
-val translate_struct_module_entry :
-  env -> module_path -> inline -> module_struct_entry ->
-  struct_expr_body (* Signature *)
-  * struct_expr_body option  (* Algebraic expr, in fact never None *)
-  * delta_resolver
-  * Univ.constraints
-
-val translate_struct_type_entry :
-  env -> inline -> module_struct_entry ->
-  struct_expr_body
-  * struct_expr_body option
-  * delta_resolver
-  * Univ.constraints
-
-val translate_struct_include_module_entry :
-  env -> module_path -> inline -> module_struct_entry ->
-  struct_expr_body
-  * struct_expr_body option (* Algebraic expr, always None *)
-  * delta_resolver
-  * Univ.constraints
+(** Low-level function for translating a module struct entry :
+    - We translate to a module when a [module_path] is given,
+      otherwise to a module type.
+    - The first output is the expanded signature
+    - The second output is the algebraic expression, kept for the extraction.
+      It is never None when translating to a module, but for module type
+      it could not be contain applications or functors.
+*)
 
-val add_modtype_constraints : env -> module_type_body -> env
+type 'alg translation =
+  module_signature * 'alg option * delta_resolver * Univ.constraints
 
-val add_module_constraints : env -> module_body -> env
+val translate_mse :
+  env -> module_path option -> inline -> module_struct_entry ->
+    module_alg_expr translation
 
-val add_struct_expr_constraints : env -> struct_expr_body -> env
-
-val struct_expr_constraints : struct_expr_body -> Univ.constraints
+val translate_mse_incl :
+  env -> module_path -> inline -> module_struct_entry ->
+    module_alg_expr translation
 
-val module_constraints : module_body -> Univ.constraints
+val finalize_module :
+  env -> module_path -> module_expression translation ->
+  (module_type_entry * inline) option ->
+  module_body
-- 
cgit v1.2.3