diff --git a/kernel/src/calculus/level.rs b/kernel/src/calculus/level.rs
index d300c4b9494c7e37d73ebe4321454a15eca65ccf..581dc22a025d97e64bdf37ae48916f63b14e7bf6 100644
--- a/kernel/src/calculus/level.rs
+++ b/kernel/src/calculus/level.rs
@@ -31,11 +31,12 @@ impl<'arena> Level<'arena> {
         }
     }
 
-    // Checks whether `self <= rhs + n`.
-    // Preicsely, it returns:
-    // - `(false, i + 1)` if `Var(i)` needs to be substituted to unstuck the comparison.
-    // - `(true, 0)` if `self <= rhs + n`,
-    // - `(false,0)` else.
+    /// Checks whether `self <= rhs + n`, without applying substitution.
+    ///
+    /// Precisely, it returns:
+    /// - `(false, i + 1)` if `Var(i)` needs to be substituted to unstuck the comparison.
+    /// - `(true, 0)` if `self <= rhs + n`,
+    /// - `(false, 0)` else.
     fn geq_no_subst(self, rhs: Self, n: i64) -> (bool, usize) {
         match (&*self,&*rhs) {
             (Zero, _) if n >= 0 => (true, 0),