From 51057db0e29f45faee9ba538c26bd39bad20222d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 9 Nov 2020 21:43:09 +0100
Subject: [PATCH] fix typo in wp_value_head

---
 theories/heap_lang/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 48448b358..39f21d758 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 *)
-- 
GitLab