From 35520fdf03f968765e9daa8b7c17f72f08b39f3c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Feb 2016 12:49:15 +0100
Subject: [PATCH] auth.v: do not depend on argument order of commutative

---
 program_logic/auth.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/program_logic/auth.v b/program_logic/auth.v
index 5167b9aa4..01e046048 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -39,7 +39,7 @@ Section auth.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     transitivity (▷auth_inv γ ★ auth_own γ a)%I.
     { rewrite /auth_inv -later_intro -(exist_intro a).
-      rewrite (commutative _ _ (φ _)) -associative. apply sep_mono; first done.
+      rewrite [(_ ★ φ _)%I]commutative -associative. apply sep_mono; first done.
       rewrite /auth_own -own_op auth_both_op. done. }
     rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
     by rewrite always_and_sep_l'.
-- 
GitLab