Apply 1 suggestion(s) to 1 file(s)

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.