diff --git a/iris_heap_lang/tactics.v b/iris_heap_lang/tactics.v
index 6e580eb1de8dc48c23a116c75f948a94fa83ce17..87484570cddcaebc27578a5cae06250708813981 100644
--- a/iris_heap_lang/tactics.v
+++ b/iris_heap_lang/tactics.v
@@ -65,7 +65,7 @@ Ltac inv_head_step :=
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
   | H : head_step ?e _ _ _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
-     and can thus better be avoided. *)
+     and should thus better be avoided. *)
      inversion H; subst; clear H
   end.