aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/modops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/modops.mli')
-rw-r--r--kernel/modops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 66aadd124..c4d8ab349 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -23,7 +23,7 @@ val module_type_of_module : module_path option -> module_body ->
module_type_body
val destr_functor :
- env -> struct_expr_body -> MBId.t * module_type_body * struct_expr_body
+ struct_expr_body -> MBId.t * module_type_body * struct_expr_body
val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body