diff options
| author | Emilio Jesus Gallego Arias | 2019-09-03 16:42:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-09-18 16:16:08 +0200 |
| commit | cca4665778dd799e5802594761e13b8d53502824 (patch) | |
| tree | 38105676715268d8d3fcaf4b0cb98caf3d5c8ed1 /vernac/declaremods.mli | |
| parent | 42ff3109217452853c3b853d21f09a317dd6e37d (diff) | |
[declaremods] Remove abstraction layer over module interpretation.
Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.
Improvement suggested by Gaëtan Gilbert.
Diffstat (limited to 'vernac/declaremods.mli')
| -rw-r--r-- | vernac/declaremods.mli | 45 |
1 files changed, 17 insertions, 28 deletions
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index 5c2c992825..ae84704656 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -29,32 +29,24 @@ type inline = (** Kinds of modules *) -type 'modast module_interpretor = - Environ.env -> Modintern.module_kind -> 'modast -> - Entries.module_struct_entry * Modintern.module_kind * Univ.ContextSet.t +type module_params = (lident list * (Constrexpr.module_ast * inline)) list -type 'modast module_params = - (lident list * ('modast * inline)) list - -(** [declare_module interp_modast id fargs typ exprs] - declares module [id], with structure constructed by [interp_modast] - from functor arguments [fargs], with final type [typ]. - [exprs] is usually of length 1 (Module definition with a concrete - body), but it could also be empty ("Declare Module", with non-empty [typ]), - or multiple (body of the shape M <+ N <+ ...). *) +(** [declare_module id fargs typ exprs] declares module [id], from + functor arguments [fargs], with final type [typ]. [exprs] is + usually of length 1 (Module definition with a concrete body), but + it could also be empty ("Declare Module", with non-empty [typ]), or + multiple (body of the shape M <+ N <+ ...). *) val declare_module : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_module : - 'modast module_interpretor -> bool option -> Id.t -> - 'modast module_params -> - ('modast * inline) module_signature -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) module_signature -> ModPath.t val end_module : unit -> ModPath.t @@ -66,18 +58,16 @@ val end_module : unit -> ModPath.t Similar to [declare_module], except that the types could be multiple *) val declare_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> - ('modast * inline) list -> + module_params -> + (Constrexpr.module_ast * inline) list -> + (Constrexpr.module_ast * inline) list -> ModPath.t val start_modtype : - 'modast module_interpretor -> Id.t -> - 'modast module_params -> - ('modast * inline) list -> ModPath.t + module_params -> + (Constrexpr.module_ast * inline) list -> ModPath.t val end_modtype : unit -> ModPath.t @@ -115,8 +105,7 @@ val import_modules : export:bool -> ModPath.t list -> unit (** Include *) -val declare_include : - 'modast module_interpretor -> ('modast * inline) list -> unit +val declare_include : (Constrexpr.module_ast * inline) list -> unit (** {6 ... } *) (** [iter_all_segments] iterate over all segments, the modules' |