diff options
Diffstat (limited to 'kernel/mod_typing.mli')
| -rw-r--r-- | kernel/mod_typing.mli | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 5949dad0..e74f455e 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Declarations @@ -21,16 +23,16 @@ open Names *) val translate_module : - env -> module_path -> inline -> module_entry -> module_body + env -> ModPath.t -> 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 + env -> ModPath.t -> inline -> module_type_entry -> module_type_body (** Low-level function for translating a module struct entry : - - We translate to a module when a [module_path] is given, + - We translate to a module when a [ModPath.t] is given, otherwise to a module type. - The first output is the expanded signature - The second output is the algebraic expression, kept mostly for @@ -40,14 +42,14 @@ type 'alg translation = module_signature * 'alg * delta_resolver * Univ.ContextSet.t val translate_mse : - env -> module_path option -> inline -> module_struct_entry -> + env -> ModPath.t 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 option) translation -> + env -> ModPath.t -> (module_expression option) translation -> (module_type_entry * inline) option -> module_body @@ -55,5 +57,5 @@ val finalize_module : module type given to an Include *) val translate_mse_incl : - bool -> env -> module_path -> inline -> module_struct_entry -> + bool -> env -> ModPath.t -> inline -> module_struct_entry -> unit translation |