diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 90e281762ec5be6942758bef772d57576bc0ca7c..52bf7eff8b8f452bc0ffae0a5db1fe6a7bc912db 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -12,7 +12,7 @@ From iris.proofmode Require Export tactics.
 From actris Require Export channel.
 From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 
--(** * Tactics for proving contractiveness of protocols *)
+(** * Tactics for proving contractiveness of protocols *)
 Ltac f_dist_le :=
   match goal with
   | H : _ ≡{?n}≡ _ |- _ ≡{?n'}≡ _ => apply (dist_le n); [apply H|lia]