diff --git a/modures/cmra.v b/modures/cmra.v
index 1e67403d925ca2cbcdf6ceedcee917dd5b3cbfda..8990ab978911d269095a303cb31a4c8b58e92b0e 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -83,7 +83,9 @@ Definition cmra_update `{Op A, ValidN A} (x y : A) := ∀ z n,
 Infix "⇝" := cmra_update (at level 70).
 Instance: Params (@cmra_update) 3.
 
-(** Timeless elements *)
+(** Timeless validity *)
+(* Not sure whether this is useful, see the rule [uPred_valid_elim_timeless]
+in logic.v *)
 Class ValidTimeless `{Valid A, ValidN A} (x : A) :=
   valid_timeless : validN 1 x → valid x.
 Arguments valid_timeless {_ _ _} _ {_} _.
@@ -128,7 +130,7 @@ Qed.
 Lemma cmra_unit_valid x n : ✓{n} x → ✓{n} (unit x).
 Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed.
 
-(* Timeless *)
+(** * Timeless *)
 Lemma cmra_timeless_included_l `{!CMRAExtend A} x y :
   Timeless x → ✓{1} y → x ≼{1} y → x ≼ y.
 Proof.
diff --git a/modures/logic.v b/modures/logic.v
index 2c36c23038f2e4d8177fb38de5c19c6288643124..c5e601ef2896f5a4e3d8121eb1cee009985f062e 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -694,7 +694,7 @@ Proof.
 Qed.
 Lemma uPred_valid_intro (a : M) : ✓ a → True%I ⊆ (✓ a)%I.
 Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
-Lemma uPred_valid_elim_timess (a : M) :
+Lemma uPred_valid_elim_timeless (a : M) :
   ValidTimeless a → ¬ ✓ a → (✓ a)%I ⊆ False%I.
 Proof.
   intros ? Hvalid x [|n] ??; [done|apply Hvalid].