diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 60229568a98bbe68fca7dcde6c0890803834bd82..00dd50b062134674083a25f0d2b380d9d283810f 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -72,10 +72,8 @@ Introduction of logical connectives
 
 - `iPureIntro` : turn a pure goal into a Coq goal. This tactic works for goals
   of the shape `⌜φ⌝`, `a ≡ b` on discrete OFEs, and `✓ a` on discrete cameras.
-
 - `iLeft` : left introduction of disjunction.
 - `iRight` : right introduction of disjunction.
-
 - `iSplit` : introduction of a conjunction, or separating conjunction provided
   one of the operands is persistent.
 - `iSplitL "H1 ... Hn"` : introduction of a separating conjunction. The