From 8c43dc46fc285b8147317c87f94f2b3de73f1686 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Mar 2021 16:50:54 +0100
Subject: [PATCH] fix warnings
using Tej's script from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/594#note_60292
---
theories/lang/lifting.v | 2 +-
theories/lang/tactics.v | 8 ++++----
theories/typing/base.v | 16 ++++++++--------
theories/typing/borrow.v | 6 +++---
theories/typing/cont_context.v | 2 +-
theories/typing/fixpoint.v | 10 +++++-----
theories/typing/function.v | 2 +-
theories/typing/lft_contexts.v | 8 ++++----
theories/typing/lib/cell.v | 2 +-
theories/typing/lib/refcell/ref.v | 2 +-
theories/typing/lib/refcell/refcell.v | 2 +-
theories/typing/lib/refcell/refmut.v | 2 +-
theories/typing/lib/rwlock/rwlock.v | 2 +-
theories/typing/lib/rwlock/rwlockreadguard.v | 2 +-
theories/typing/lib/rwlock/rwlockwriteguard.v | 2 +-
theories/typing/own.v | 4 ++--
theories/typing/product.v | 4 ++--
theories/typing/product_split.v | 8 ++++----
theories/typing/shr_bor.v | 2 +-
theories/typing/sum.v | 4 ++--
theories/typing/type.v | 6 +++---
theories/typing/type_context.v | 12 ++++++------
theories/typing/type_sum.v | 2 +-
theories/typing/uninit.v | 2 +-
theories/typing/uniq_bor.v | 4 ++--
25 files changed, 58 insertions(+), 58 deletions(-)
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 7a642217..93b47498 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -47,7 +47,7 @@ Proof. by unlock. Qed.
Class DoSubst (x : binder) (es : expr) (e er : expr) :=
do_subst : subst' x es e = er.
-Hint Extern 0 (DoSubst _ _ _ _) =>
+Global Hint Extern 0 (DoSubst _ _ _ _) =>
rewrite /DoSubst; simpl_subst; reflexivity : typeclass_instances.
Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 0887d4d7..e49c8111 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -175,7 +175,7 @@ Ltac solve_closed :=
let e' := W.of_expr e in change (Closed X (W.to_expr e'));
apply W.is_closed_correct; vm_compute; exact I
end.
-Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
+Global Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Ltac solve_into_val :=
match goal with
@@ -184,7 +184,7 @@ Ltac solve_into_val :=
apply W.to_val_Some; simpl; unfold W.to_expr;
((unlock; exact eq_refl) || (idtac; exact eq_refl))
end.
-Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
+Global Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
Ltac solve_as_val :=
match goal with
@@ -192,7 +192,7 @@ Ltac solve_as_val :=
let e' := W.of_expr e in change (∃ v, of_val v = W.to_expr e');
apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end.
-Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
+Global Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
Ltac solve_atomic :=
match goal with
@@ -200,7 +200,7 @@ Ltac solve_atomic :=
let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
apply W.is_atomic_correct; vm_compute; exact I
end.
-Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
+Global Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
Global Instance skip_atomic : Atomic WeaklyAtomic Skip.
Proof.
diff --git a/theories/typing/base.v b/theories/typing/base.v
index f5a8b002..f5cb2484 100644
--- a/theories/typing/base.v
+++ b/theories/typing/base.v
@@ -20,18 +20,18 @@ Ltac solve_typing :=
(typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
(typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
-Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
-Hint Resolve submseteq_cons submseteq_inserts_l submseteq_inserts_r
+Global Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
+Global Hint Resolve submseteq_cons submseteq_inserts_l submseteq_inserts_r
: lrust_typing.
-Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
+Global Hint Extern 1 (@eq nat _ (Z.to_nat _)) =>
(etrans; [symmetry; exact: Nat2Z.id | reflexivity]) : lrust_typing.
-Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
+Global Hint Extern 1 (@eq nat (Z.to_nat _) _) =>
(etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
-Hint Resolve <- elem_of_app : lrust_typing.
+Global Hint Resolve <- elem_of_app : lrust_typing.
(* done is there to handle equalities with constants *)
-Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : lrust_typing.
-Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : lrust_typing.
-Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.
+Global Hint Extern 100 (_ ≤ _) => simpl; first [done|lia] : lrust_typing.
+Global Hint Extern 100 (@eq Z _ _) => simpl; first [done|lia] : lrust_typing.
+Global Hint Extern 100 (@eq nat _ _) => simpl; first [done|lia] : lrust_typing.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 2df1328b..baf447ff 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -212,7 +212,7 @@ Section borrow.
Proof. iIntros. iApply type_let; [by apply type_deref_shr_uniq_instr|solve_typing|done]. Qed.
End borrow.
-Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
+Global Hint Resolve tctx_extract_hasty_borrow tctx_extract_hasty_borrow_share
| 10 : lrust_typing.
-Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
-Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_share | 10 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_share_samelft | 9 : lrust_typing.
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index 11843498..b76fdf65 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -116,4 +116,4 @@ Section cont_context.
Qed.
End cont_context.
-Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
+Global Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 3efd7862..76c9e197 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -141,11 +141,11 @@ Section subtyping.
Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
End subtyping.
-Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
+Global Hint Resolve fixpoint_mono fixpoint_proper : lrust_typing.
(* These hints can loop if [fixpoint_mono] and [fixpoint_proper] have
not been tried before, so we give them a high cost *)
-Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
-Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_subtype_l|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_subtype_r|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_eqtype_l|100 : lrust_typing.
+Global Hint Resolve fixpoint_unfold_eqtype_r|100 : lrust_typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index fac54aac..534f80e5 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -444,4 +444,4 @@ Section typing.
Qed.
End typing.
-Hint Resolve fn_subtype : lrust_typing.
+Global Hint Resolve fn_subtype : lrust_typing.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 2525bdfc..268f972b 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -419,7 +419,7 @@ Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ} E E' L :
E' ⊆+ E → elctx_sat E L E'.
Proof. iIntros (HE' ??) "_ !# H". by iApply big_sepL_submseteq. Qed.
-Hint Resolve
+Global Hint Resolve
lctx_lft_incl_refl lctx_lft_incl_static lctx_lft_incl_local'
lctx_lft_incl_external' lctx_lft_incl_intersect
lctx_lft_incl_intersect_l lctx_lft_incl_intersect_r
@@ -427,8 +427,8 @@ Hint Resolve
elctx_sat_nil elctx_sat_lft_incl elctx_sat_app elctx_sat_refl
: lrust_typing.
-Hint Extern 10 (lctx_lft_eq _ _ _ _) => split : lrust_typing.
+Global Hint Extern 10 (lctx_lft_eq _ _ _ _) => split : lrust_typing.
-Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.
+Global Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.
-Hint Opaque elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
+Global Hint Opaque elctx_sat lctx_lft_alive lctx_lft_incl : lrust_typing.
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index ae86479b..b0e90f84 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -253,4 +253,4 @@ Section typing.
Qed.
End typing.
-Hint Resolve cell_mono' cell_proper' : lrust_typing.
+Global Hint Resolve cell_mono' cell_proper' : lrust_typing.
diff --git a/theories/typing/lib/refcell/ref.v b/theories/typing/lib/refcell/ref.v
index f50312d3..ccbcbb47 100644
--- a/theories/typing/lib/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -113,4 +113,4 @@ Section ref.
Proof. intros. by eapply ref_proper. Qed.
End ref.
-Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
+Global Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index b089b73d..23ad8be5 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -209,4 +209,4 @@ Section refcell.
Proof. move=>???[|[[]|]]//=. Qed.
End refcell.
-Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
+Global Hint Resolve refcell_mono' refcell_proper' : lrust_typing.
diff --git a/theories/typing/lib/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
index 3da42ad7..9a0be7e7 100644
--- a/theories/typing/lib/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -125,4 +125,4 @@ Section refmut.
Proof. intros. by eapply refmut_proper. Qed.
End refmut.
-Hint Resolve refmut_mono' refmut_proper' : lrust_typing.
+Global Hint Resolve refmut_mono' refmut_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 889ec4d1..c462ce0b 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -226,4 +226,4 @@ Section rwlock.
Qed.
End rwlock.
-Hint Resolve rwlock_mono' rwlock_proper' : lrust_typing.
+Global Hint Resolve rwlock_mono' rwlock_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index e33822fc..e39ef044 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -137,4 +137,4 @@ Section rwlockreadguard.
Qed.
End rwlockreadguard.
-Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.
+Global Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 0342b547..5b348f3d 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -143,4 +143,4 @@ Section rwlockwriteguard.
Qed.
End rwlockwriteguard.
-Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
+Global Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 3de55448..2d246eb1 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -362,8 +362,8 @@ Section typing.
Qed.
End typing.
-Hint Resolve own_mono' own_proper' box_mono' box_proper'
+Global Hint Resolve own_mono' own_proper' box_mono' box_proper'
write_own read_own_copy : lrust_typing.
(* By setting the priority high, we make sure copying is tried before
moving. *)
-Hint Resolve read_own_move | 100 : lrust_typing.
+Global Hint Resolve read_own_move | 100 : lrust_typing.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index d1d5b103..60503985 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -262,6 +262,6 @@ Section typing.
End typing.
Arguments product : simpl never.
-Hint Opaque product : lrust_typing lrust_typing_merge.
-Hint Resolve product_mono' product_proper' ty_outlives_E_elctx_sat_product
+Global Hint Opaque product : lrust_typing lrust_typing_merge.
+Global Hint Resolve product_mono' product_proper' ty_outlives_E_elctx_sat_product
: lrust_typing.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 3c2ff90b..8e3e8ec2 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -302,11 +302,11 @@ End product_split.
(* We do not want unification to try to unify the definition of these
types with anything in order to try splitting or merging. *)
-Hint Opaque own_ptr uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
+Global Hint Opaque own_ptr uniq_bor shr_bor tctx_extract_hasty : lrust_typing lrust_typing_merge.
(* We make sure that splitting is tried before borrowing, so that not
the entire product is borrowed when only a part is needed. *)
-Hint Resolve tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extract_split_shr_prod
+Global Hint Resolve tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extract_split_shr_prod
| 5 : lrust_typing.
(* Merging is also tried after everything, except
@@ -319,6 +319,6 @@ Hint Resolve tctx_extract_split_own_prod tctx_extract_split_uniq_prod tctx_extra
solve_typing get slow because of that. See:
https://coq.inria.fr/bugs/show_bug.cgi?id=5304
*)
-Hint Resolve tctx_extract_merge_own_prod tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
+Global Hint Resolve tctx_extract_merge_own_prod tctx_extract_merge_uniq_prod tctx_extract_merge_shr_prod
| 40 : lrust_typing_merge.
-Hint Unfold extract_tyl : lrust_typing.
+Global Hint Unfold extract_tyl : lrust_typing.
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 18b0c817..471a6775 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -98,4 +98,4 @@ Section typing.
Qed.
End typing.
-Hint Resolve shr_mono' shr_proper' read_shr : lrust_typing.
+Global Hint Resolve shr_mono' shr_proper' read_shr : lrust_typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 55e1a493..ebf0d432 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -240,5 +240,5 @@ End sum.
Notation "Σ[ ty1 ; .. ; tyn ]" :=
(sum (cons ty1%T (..(cons tyn%T nil)..))) : lrust_type_scope.
-Hint Opaque sum : lrust_typing lrust_typing_merge.
-Hint Resolve sum_mono' sum_proper' : lrust_typing.
+Global Hint Opaque sum : lrust_typing lrust_typing_merge.
+Global Hint Resolve sum_mono' sum_proper' : lrust_typing.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index aa1c630d..384c1089 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -757,6 +757,6 @@ Section type_util.
End type_util.
-Hint Resolve ty_outlives_E_elctx_sat tyl_outlives_E_elctx_sat : lrust_typing.
-Hint Resolve subtype_refl eqtype_refl : lrust_typing.
-Hint Opaque subtype eqtype : lrust_typing.
+Global Hint Resolve ty_outlives_E_elctx_sat tyl_outlives_E_elctx_sat : lrust_typing.
+Global Hint Resolve subtype_refl eqtype_refl : lrust_typing.
+Global Hint Opaque subtype eqtype : lrust_typing.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index ce685e63..d77939a3 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -319,17 +319,17 @@ Section type_context.
Qed.
End type_context.
-Hint Resolve tctx_extract_hasty_here_copy | 1 : lrust_typing.
-Hint Resolve tctx_extract_hasty_here | 20 : lrust_typing.
-Hint Resolve tctx_extract_hasty_further | 50 : lrust_typing.
-Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
+Global Hint Resolve tctx_extract_hasty_here_copy | 1 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_here | 20 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_further | 50 : lrust_typing.
+Global Hint Resolve tctx_extract_blocked_here tctx_extract_blocked_cons
tctx_extract_ctx_nil tctx_extract_ctx_hasty
tctx_extract_ctx_blocked tctx_extract_ctx_incl : lrust_typing.
-Hint Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked
+Global Hint Opaque tctx_extract_ctx tctx_extract_hasty tctx_extract_blocked
tctx_incl : lrust_typing.
(* In general, we want reborrowing to be tried before subtyping, so
that we get the extraction. However, in the case the types match
exactly, we want to NOT use reborrowing. Therefore, we add
[tctx_extract_hasty_here_eq] as a hint with a very low cost. *)
-Hint Resolve tctx_extract_hasty_here_eq | 2 : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_here_eq | 2 : lrust_typing.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index b0a513f9..9c4f033e 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -294,4 +294,4 @@ Section case.
Qed.
End case.
-Hint Resolve ty_outlives_E_elctx_sat_sum : lrust_typing.
+Global Hint Resolve ty_outlives_E_elctx_sat_sum : lrust_typing.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index 214c359f..bddc9622 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -132,7 +132,7 @@ Section uninit.
Proof. rewrite -uninit_uninit0_eqtype=>->//. Qed.
End uninit.
-Hint Resolve uninit_product_eqtype_cons_l uninit_product_eqtype_cons_r
+Global Hint Resolve uninit_product_eqtype_cons_l uninit_product_eqtype_cons_r
uninit_product_subtype_cons_l uninit_product_subtype_cons_r
uninit_unit_eqtype uninit_unit_eqtype'
uninit_unit_subtype uninit_unit_subtype' : lrust_typing.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 0c747e29..badff4b2 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -173,5 +173,5 @@ Section typing.
Qed.
End typing.
-Hint Resolve uniq_mono' uniq_proper' write_uniq read_uniq : lrust_typing.
-Hint Resolve tctx_extract_hasty_reborrow | 10 : lrust_typing.
+Global Hint Resolve uniq_mono' uniq_proper' write_uniq read_uniq : lrust_typing.
+Global Hint Resolve tctx_extract_hasty_reborrow | 10 : lrust_typing.
--
GitLab