diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 1d6861cdb40701df1cb9b112df7116613066c535..7ab1f4c18447b4164959a282d8c0f5c82a65f7fd 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -520,7 +520,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
   if decide (op = EqOp) then
     (* Crucially, this compares the same way as [CmpXchg]! *)
-    if bool_decide (vals_compare_safe v1 v2) then
+    if decide (vals_compare_safe v1 v2) then
       Some $ LitV $ LitBool $ bool_decide (v1 = v2)
     else
       None
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 8dda1c8f27c9f92c557b1f97fe0131b2bbf4f96d..48b9cbe700adc485f7436bed3ee1fdba90ee75d1 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -172,7 +172,7 @@ Proof.
   intros Hcompare.
   cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
   { intros. revert Hcompare. solve_pure_exec. }
-  rewrite /bin_op_eval /= bool_decide_true //.
+  rewrite /bin_op_eval /= decide_True //.
 Qed.
 
 Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.