From d96622742743e8a24eff3b3960d6756b0e39fc08 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 8 Nov 2019 16:42:33 +0100
Subject: [PATCH] Make ambigious argument explicit.

To prepare for https://github.com/coq/coq/pull/10762
---
 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 8fbfcdddf..f302796be 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -622,7 +622,7 @@ Qed.
 Global Instance id_free_op_r x y : IdFree y → Cancelable x → IdFree (x ⋅ y).
 Proof.
   intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
-  eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto].
+  eapply (id_free0_r y); [by eapply cmra_validN_op_r |symmetry; eauto].
 Qed.
 Global Instance id_free_op_l x y : IdFree x → Cancelable y → IdFree (x ⋅ y).
 Proof. intros. rewrite comm. apply _. Qed.
-- 
GitLab