From aac8c9ef7ecd95cbbf44792201d10be60c1ac54a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Mar 2018 13:21:40 +0100
Subject: [PATCH] Fix typo.
---
theories/heap_lang/proofmode.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index d4474c3fb..6468daddc 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -70,7 +70,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
|apply _ (* IntoLaters *)
|wp_expr_simpl_subst; try wp_value_head (* new goal *)
])
- || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+ || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
let e := eval simpl in e in
reshape_expr e ltac:(fun K e' =>
@@ -80,7 +80,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
|try fast_done (* The pure condition for PureExec *)
|wp_expr_simpl_subst; try wp_value_head (* new goal *)
])
- || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+ || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"
| _ => fail "wp_pure: not a 'wp'"
end.
--
GitLab