From 3875c72637ea550e8a4b36c8002a36072cb65236 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Jun 2017 09:56:26 +0200
Subject: [PATCH] Give from_op_op a lower precedence so that it is not picked
 by default when using iCombine.

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

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index f8ba7a8e1..f30a4c0a7 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -389,7 +389,7 @@ Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M
 Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
 
 (* FromOp *)
-Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a â‹… b) a b.
+Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a â‹… b) a b | 100.
 Proof. by rewrite /FromOp. Qed.
 
 (* TODO: Worst case there could be a lot of backtracking on these instances,
-- 
GitLab