Support tighter precedence for x.1, x.2 notation.

bc5689ac · David Swasey · e6ec2867 · bc5689ac
Commit bc5689ac authored Nov 29, 2017 by David Swasey
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

theories/algebra/cmra.v theories/algebra/cmra.v +1 -1

No files found.
--- 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.