diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 51aaf2c9326a8243ce4b6badf5d1a3cd8c2dca39..91603b0c74efb5308961152f17212c434b0f6b87 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -2,12 +2,11 @@ From iris.heap_lang Require Export substitution.
 From iris.prelude Require Import fin_maps.
 Import heap_lang.
 
-(** The tactic [inv_step] performs inversion on hypotheses of the shape
-[prim_step] and [head_step]. For hypotheses of the shape [prim_step] it will
-decompose the evaluation context. The tactic will discharge
-head-reductions starting from values, and simplifies hypothesis related
-to conversions from and to values, and finite map operations. This tactic is
-slightly ad-hoc and tuned for proving our lifting lemmas. *)
+(** The tactic [inv_step] performs inversion on hypotheses of the
+shape [head_step]. The tactic will discharge head-reductions starting
+from values, and simplifies hypothesis related to conversions from and
+to values, and finite map operations. This tactic is slightly ad-hoc
+and tuned for proving our lifting lemmas. *)
 Ltac inv_step :=
   repeat match goal with
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)
@@ -64,11 +63,10 @@ Ltac reshape_expr e tac :=
   | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
   end in go (@nil ectx_item) e.
 
-(** The tactic [do_step tac] solves goals of the shape [reducible], [prim_step]
-and [head_step] by performing a reduction step and uses [tac] to solve any
-side-conditions generated by individual steps. In case of goals of the shape
-[reducible] and [prim_step], it will try to decompose to expression on the LHS
-into an evaluation context and head-redex. *)
+(** The tactic [do_step tac] solves goals of the shape
+[head_reducible] and [head_step] by performing a reduction step and
+uses [tac] to solve any side-conditions generated by individual
+steps. *)
 Tactic Notation "do_step" tactic3(tac) :=
   try match goal with |- head_reducible _ _ => eexists _, _, _ end;
   simpl;