From e423686f1135fa84a4c136c73b84fc67cf94a144 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Jul 2016 16:54:23 +0200
Subject: [PATCH] =?UTF-8?q?Give=20the=20left=20instance=20of=20FromAnd=20(?=
 =?UTF-8?q?P1=20=E2=98=85=20P2)=20P1=20P2=20precedence.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

That way type class search becomes more predictable.
---
 proofmode/classes.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/proofmode/classes.v b/proofmode/classes.v
index b30f4311c..b8d444380 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -112,10 +112,10 @@ Global Arguments from_and : clear implicits.
 Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
 Proof. done. Qed.
 Global Instance from_and_sep_persistent_l P1 P2 :
-  PersistentP P1 → FromAnd (P1 ★ P2) P1 P2.
+  PersistentP P1 → FromAnd (P1 ★ P2) P1 P2 | 9.
 Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
 Global Instance from_and_sep_persistent_r P1 P2 :
-  PersistentP P2 → FromAnd (P1 ★ P2) P1 P2.
+  PersistentP P2 → FromAnd (P1 ★ P2) P1 P2 | 10.
 Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
 Global Instance from_and_always P Q1 Q2 :
   FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
-- 
GitLab