aboutsummaryrefslogtreecommitdiff
path: root/parsing/astmod.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/astmod.mli')
-rw-r--r--parsing/astmod.mli11
1 files changed, 3 insertions, 8 deletions
diff --git a/parsing/astmod.mli b/parsing/astmod.mli
index 158f40e890..49e061a0be 100644
--- a/parsing/astmod.mli
+++ b/parsing/astmod.mli
@@ -19,12 +19,7 @@ open Evd
(* Module expressions and module types are interpreted relatively to
eventual functor or funsig arguments. *)
-val interp_module_decl : evar_map -> env ->
- (identifier list * Coqast.t) list ->
- Coqast.t option ->
- Coqast.t option
- ->
- (identifier * (mod_bound_id * module_type_entry)) list *
- module_type_entry option *
- module_expr option
+val interp_modtype : env -> Coqast.t -> module_type_entry
+
+val interp_modexpr : env -> Coqast.t -> module_expr