diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index d4474c3fb66ae3b2a6acbfa84f9eece2c4098965..6468daddcb8d55679869e81ee972dee492e2cee0 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.