From bc5689acacbbf622d6f8072202a908dae0aa806c Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Wed, 29 Nov 2017 16:01:21 +0100
Subject: [PATCH] Support tighter precedence for x.1, x.2 notation.

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

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 91d626f83..cd042a56e 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1514,7 +1514,7 @@ Section ofe_fun_cmra.
       { intros x. specialize (Hf12 x).
         destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
         exists (y1,y2); eauto. }
-      exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
+      exists (λ x, (gg x).1), (λ x, (gg x).2). split_and!=> -?; naive_solver.
   Qed.
   Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin.
 
-- 
GitLab