diff git a/docs/proof_mode.md b/docs/proof_mode.md
index 00dd50b062134674083a25f0d2b380d9d283810f..a80b31ff3c3de02a5655105e25fc9bb18134f82c 100644
 a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ 108,17 +108,13 @@ Separation logicspecific tactics
 `iFrame (t1 .. tn) "selpat"` : cancel the Coq terms (or Coq hypotheses)
`t1 ... tn` and Iris hypotheses given by `selpat` in the goal. The constructs
of the selection pattern have the following meaning:

+ `%` : repeatedly frame hypotheses from the Coq context.
+ `#` : repeatedly frame hypotheses from the intuitionistic context.
+ `∗` : frame as much of the spatial context as possible. (N.B: this
is the unicode symbol `∗`, not the regular asterisk `*`.)

Notice that framing spatial hypotheses makes them disappear, but framing Coq
or intuitionistic hypotheses does not make them disappear.

 This tactic solves the goal if everything in the conclusion has been
 framed.
+ This tactic solves the goal if everything in the conclusion has been framed.
 `iCombine "H1" "H2" as "pat"` : combines `H1 : P1` and `H2 : P2` into
`H: P1 ∗ P2`, then calls `iDestruct H as pat` on the combined hypothesis.
 `iAccu` : solves a goal that is an evar by instantiating it with a all
@@ 176,7 +172,6 @@ Rewriting / simplification
goal / hypotheses given by the selection pattern `selpat`. This is a
shorthand for `iEval (simpl)`.

Iris
