From ec42e1d060e2a309548f386bda787a0c24c8147a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sun, 4 Mar 2018 00:09:45 +0100
Subject: [PATCH] Fix build by being a little bit less restrictive in Hint
 Modes.

---
 theories/bi/embedding.v | 3 ++-
 theories/bi/plainly.v   | 2 +-
 theories/bi/updates.v   | 6 +++---
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 2ba22584a..67a798964 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -38,7 +38,8 @@ Class SbiEmbed (PROP1 PROP2 : sbi) `{BiEmbed PROP1 PROP2} := {
   embed_later P : ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤;
   embed_interal_inj (PROP' : sbi) (P Q : PROP1) : ⎡P⎤ ≡ ⎡Q⎤ ⊢ (P ≡ Q : PROP');
 }.
-Hint Mode SbiEmbed + + ! : typeclass_instances.
+Hint Mode SbiEmbed ! - - : typeclass_instances.
+Hint Mode SbiEmbed - ! - : typeclass_instances.
 
 Section embed_laws.
   Context `{BiEmbed PROP1 PROP2}.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 06fff510d..a3c7d83fb 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -48,7 +48,7 @@ Class BiPlainlyExist `{!BiPlainly PROP} :=
 Arguments BiPlainlyExist : clear implicits.
 Arguments BiPlainlyExist _ {_}.
 Arguments plainly_exist_1 _ {_ _} _.
-Hint Mode BiPlainlyExist + ! : typeclass_instances.
+Hint Mode BiPlainlyExist ! - : typeclass_instances.
 
 Section plainly_laws.
   Context `{BiPlainly PROP}.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 2a5fff709..40669d751 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -87,11 +87,11 @@ Arguments bi_fupd_fupd : simpl never.
 
 Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} :=
   bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
-Hint Mode BiBUpdFUpd + ! ! : typeclass_instances.
+Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
 Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
   bupd_plainly (P : PROP) : (|==> ■ P) -∗ P.
-Hint Mode BiBUpdPlainly + ! ! : typeclass_instances.
+Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
 
 Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
   fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
@@ -100,7 +100,7 @@ Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
   later_fupd_plain E (P : PROP) `{!Plain P} :
     (▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
 }.
-Hint Mode BiBUpdFUpd + ! ! : typeclass_instances.
+Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
 Section bupd_laws.
   Context `{BiBUpd PROP}.
-- 
GitLab