blob: 21171705de5f6990e7446a85bd096122a127b431 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Declarations
open Environ
open Entries
open Mod_subst
open Names
(** Main functions for translating module entries
Note : [module_body] and [module_type_body] obtained this way
won't have any [MEstruct] in their algebraic fields.
*)
val translate_module :
env -> module_path -> inline -> module_entry -> module_body
val translate_modtype :
env -> module_path -> 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,
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.
Moreover algebraic expressions obtained here cannot contain [MEstruct].
*)
type 'alg translation =
module_signature * 'alg option * delta_resolver * Univ.constraints
val translate_mse :
env -> module_path option -> inline -> module_struct_entry ->
module_alg_expr translation
val translate_mse_incl :
env -> module_path -> inline -> module_struct_entry ->
module_alg_expr translation
val finalize_module :
env -> module_path -> module_expression translation ->
(module_type_entry * inline) option ->
module_body
|
