aboutsummaryrefslogtreecommitdiff
path: root/kernel/modops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/modops.ml')
-rw-r--r--kernel/modops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4fdd7ab334..472fddb829 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -515,7 +515,7 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
"Module M:=P." or "Module M. Include P. End M."
We need to perform two operations to compute the body of M.
- The first one is applying the substitution {P <- M} on the type of P
- - The second one is strenghtening. *)
+ - The second one is strengthening. *)
let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
|NoFunctor struc ->