From 10d74380d59bdbf32d550f626c84ffb811ae9142 Mon Sep 17 00:00:00 2001
From: Robbert <gitlab-sws@robbertkrebbers.nl>
Date: Thu, 7 Jan 2021 09:37:04 +0100
Subject: [PATCH] Apply 1 suggestion(s) to 1 file(s)
---
iris_heap_lang/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/iris_heap_lang/tactics.v b/iris_heap_lang/tactics.v
index 6e580eb1d..87484570c 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.
--
GitLab