diff options
Diffstat (limited to 'kernel/mod_typing.mli')
| -rw-r--r-- | kernel/mod_typing.mli | 26 |
1 files changed, 18 insertions, 8 deletions
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 |