diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 48448b35801d1330b185530d4198f55e42961573..39f21d758b1be6aa9a7873f715b9b89832dcb966 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -56,7 +56,7 @@ Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 
 Ltac wp_value_head :=
-  first [eapply tac_wp_value || eapply tac_twp_value].
+  first [eapply tac_wp_value | eapply tac_twp_value].
 
 Ltac wp_finish :=
   wp_expr_simpl;      (* simplify occurences of subst/fill *)