From aa086f741b7612c6644755c42507f5b1f9d541a1 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <au688989@d45276.eduroam.net.au.dk>
Date: Wed, 16 Jun 2021 16:36:26 +0200
Subject: [PATCH] Added scope of unscoped hint modes to address deprecation
 warning

---
 theories/channel/proofmode.v      | 6 +++---
 theories/channel/proto.v          | 4 ++--
 theories/logrel/session_types.v   | 2 +-
 theories/logrel/subtyping_rules.v | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 8f4294b..8750ba4 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -24,7 +24,7 @@ Ltac solve_proto_contractive :=
 (** * Normalization of protocols *)
 Class ActionDualIf (d : bool) (a1 a2 : action) :=
   dual_action_if : a2 = if d then action_dual a1 else a1.
-Hint Mode ActionDualIf ! ! - : typeclass_instances.
+Global Hint Mode ActionDualIf ! ! - : typeclass_instances.
 
 Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
 Instance action_dual_if_true_send : ActionDualIf true Send Recv := eq_refl.
@@ -35,7 +35,7 @@ Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
   proto_normalize :
     ⊢ iProto_dual_if d p <++>
         foldr (iProto_app ∘ curry iProto_dual_if) END%proto pas ⊑ q.
-Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
+Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
 Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.
 
 Notation ProtoUnfold p1 p2 := (∀ d pas q,
@@ -45,7 +45,7 @@ Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
     (pas : list (bool * iProto Σ)) (m2 : iMsg Σ) :=
   msg_normalize a :
     ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
-Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
+Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
 Arguments MsgNormalize {_} _ _%msg _%msg _%msg.
 
 Section classes.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 2c91fda..111c9ee 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -191,7 +191,7 @@ Notation "<?.. x1 .. xn > m" := (<?> ∃.. x1, .. (∃.. xn, m) ..)
 Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
     (tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
   msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
-Hint Mode MsgTele ! ! - ! - - - : typeclass_instances.
+Global Hint Mode MsgTele ! ! - ! - - - : typeclass_instances.
 
 (** * Operations *)
 Program Definition iMsg_map {Σ V}
@@ -1295,5 +1295,5 @@ End proto.
 
 Typeclasses Opaque iProto_ctx iProto_own.
 
-Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
+Global Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
   first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 1a79e7d..d04230c 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -78,7 +78,7 @@ Notation "(.<++> T )" := (λ S, lty_app S T) (only parsing) : lty_scope.
 Class LtyMsgTele {Σ} {kt : ktele Σ} (M : lmsg Σ)
     (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) :=
   lty_msg_tele : M ≡ (∃.. x, TY ktele_app A x; ktele_app S x)%lmsg.
-Hint Mode LtyMsgTele ! - ! - - : typeclass_instances.
+Global Hint Mode LtyMsgTele ! - ! - - : typeclass_instances.
 
 Section session_types.
   Context {Σ : gFunctors}.
diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index 321edfd..7ee3bfc 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -606,5 +606,5 @@ Section subtyping_rules.
 
 End subtyping_rules.
 
-Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>
+Global Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>
   first [is_evar x; fail 1 | is_evar y; fail 1|iApply lty_le_refl] : core.
-- 
GitLab