From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 26 Jan 2016 16:56:33 +0100
Subject: Imported Upstream version 8.5

---
 kernel/mod_typing.mli | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

(limited to 'kernel/mod_typing.mli')

diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index bc0e2020..5949dad0 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-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -14,9 +14,18 @@ open Names
 
 (** Main functions for translating module entries *)
 
+(** [translate_module] produces a [module_body] out of a [module_entry].
+    In the output fields:
+    - [mod_expr] is [Abstract] for a [MType] entry, or [Algebraic] for [MExpr].
+    - [mod_type_alg] is [None] only for a [MExpr] without explicit signature.
+*)
+
 val translate_module :
   env -> module_path -> inline -> module_entry -> module_body
 
+(** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
+    cannot be [None] (and of course [mod_expr] is [Abstract]). *)
+
 val translate_modtype :
   env -> module_path -> inline -> module_type_entry -> module_type_body
 
@@ -24,20 +33,21 @@ val translate_modtype :
     - 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.
-*)
+    - The second output is the algebraic expression, kept mostly for
+      the extraction. *)
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
+  module_signature * 'alg * delta_resolver * Univ.ContextSet.t
 
 val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
     module_alg_expr translation
 
+(** From an already-translated (or interactive) implementation and
+    an (optional) signature entry, produces a final [module_body] *)
+
 val finalize_module :
-  env -> module_path -> module_expression translation ->
+  env -> module_path -> (module_expression option) translation ->
   (module_type_entry * inline) option ->
   module_body
 
@@ -46,4 +56,4 @@ val finalize_module :
 
 val translate_mse_incl :
   bool -> env -> module_path -> inline -> module_struct_entry ->
-    module_alg_expr translation
+    unit translation
-- 
cgit v1.2.3