aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/environ.mli')
-rw-r--r--kernel/environ.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ffa3ceb87..0dcc291b5 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -143,10 +143,10 @@ val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
(** {5 Modules } *)
-val add_modtype : module_path -> module_type_body -> env -> env
+val add_modtype : module_type_body -> env -> env
(** [shallow_add_module] does not add module components *)
-val shallow_add_module : module_path -> module_body -> env -> env
+val shallow_add_module : module_body -> env -> env
val lookup_module : module_path -> env -> module_body
val lookup_modtype : module_path -> env -> module_type_body