aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/univ.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1914ce5e34..f7c984870f 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -322,7 +322,7 @@ val in_punivs : 'a -> 'a puniverses
val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
(** A vector of universe levels with universe Constraint.t,
- representiong local universe variables and associated Constraint.t *)
+ representing local universe variables and associated Constraint.t *)
module UContext :
sig