diff --git a/README.md b/README.md
index 13f11fee4377111981486f8dc74f51af15c9a83b..e85a1cdac0d05a91d00b23df01fc29aed5013249 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ This repository contains the main Coq specification & proof development of the [
 
 ## Documentation
 
-Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homeage:
+Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homepage:
 
 - <https://prosa.mpi-sws.org/branches>
 
diff --git a/doc/tactics.md b/doc/tactics.md
index 56a6638db794f104749ef6f0773dd52eea08a7ce..3c46e4481b5b842207ff1229293ad9b0d1bac915 100644
--- a/doc/tactics.md
+++ b/doc/tactics.md
@@ -19,19 +19,19 @@ Tactics taken from the standard library of Viktor Vafeiadis.
 
 - `desf_asm`: same as `desf`, but only applied to the assumptions in the local context.
 
-- `exploit H`: When applied to a hypothesis/lemma H, converts pre-conditions into goals in order to infer the post-condition of H, which is then added to the local context.
+- `exploit H`: When applied to a hypothesis/lemma `H`, converts pre-conditions into goals in order to infer the post-condition of `H`, which is then added to the local context.
 
-- `feed H`: Same as exploit, but only generates a goal for the first pre-condition. That is, applying exploit to (H: P1 -> P2 -> P3) produces (H: P2 -> P3) and converts P1 into a goal. This is useful for cleaning up induction hypotheses.
+- `feed H`: Same as exploit, but only generates a goal for the first pre-condition. That is, applying exploit to `H: P1 -> P2 -> P3` produces `H: P2 -> P3` and converts `P1` into a goal. This is useful for cleaning up induction hypotheses.
 
-- `feed_n k H`: Same as feed, but generates goals up to the k-th pre-condition.
+- `feed_n k H`: Same as feed, but generates goals up to the `k`-th pre-condition.
 
-- `specialize (H x1 x2 x3)`: instantiates hypothesis H in place with values x1, x2, x3.
+- `specialize (H x1 x2 x3)`: instantiates hypothesis `H` in place with values `x1`, `x2`, and `x3`.
 
 *To be continued… please help out.*
 
 ## Tactics from `ssreflect`
 
-- `have y := f x1 x2 x3`: Creates an alias to (f x1 x2 x3) called y (in the local context). Note that f can be a function or a proposition/lemma.
+- `have y := f x1 x2 x3`: Creates an alias to `f x1 x2 x3` called `y` (in the local context). Note that `f` can be a function or a proposition/lemma. It's usually easier to read than `move: (f x1 x2 x3) => y`.
 
 *To be written… please feel free to start.*
 
@@ -40,3 +40,7 @@ Tactics taken from the standard library of Viktor Vafeiadis.
 
 *To be written… please feel free to start.*
 
+## Miscellaneous
+
+- `ssrlia`: Solves arithmetic goals, including ones with `ssreflect`'s definitions.
+
diff --git a/util/ssrlia.v b/util/ssrlia.v
index e24e726fc4c773e3f9631d625ae782d0ff1a5214..469fed3d8610274417b8868d47d2748c032c1424 100644
--- a/util/ssrlia.v
+++ b/util/ssrlia.v
@@ -24,6 +24,10 @@ Ltac arith_goal_ssrnat2coqnat :=
     | |- is_true (_ < _) => try apply/ltP
   end.
 
+(** Solve arithmetic goals.
+  This tactic first rewrites the context to replace ssreflect's operations
+  to the corresponding operations in the Coq library, then calls [lia]. *)
+
 Ltac ssrlia :=
   repeat arith_hypo_ssrnat2coqnat;
   arith_goal_ssrnat2coqnat; simpl;