diff --git a/src/riscv/Examples/Example64Literal.v b/src/riscv/Examples/Example64Literal.v
index e15e726..2670930 100644
--- a/src/riscv/Examples/Example64Literal.v
+++ b/src/riscv/Examples/Example64Literal.v
@@ -19,7 +19,7 @@ Require Import riscv.Utility.DefaultMemImpl64.
 Require Import coqutil.Map.Z_keyed_SortedListMap.
 Require coqutil.Map.SortedList.
 
-Existing Instance DefaultRiscvState.
+#[global] Existing Instance DefaultRiscvState.
 
 
 Definition foo7prog: list MachineInt := [
diff --git a/src/riscv/Examples/MulTrapHandler.v b/src/riscv/Examples/MulTrapHandler.v
index 820c5e2..701f78b 100644
--- a/src/riscv/Examples/MulTrapHandler.v
+++ b/src/riscv/Examples/MulTrapHandler.v
@@ -73,7 +73,7 @@ Definition initial_state: State := HNil
                         (CSRField.MScratch, handler_stack_start) :: nil)]
   [exectrace := nil].
 
-Instance IsRiscvMachine: RiscvProgram (StateAbortFail State) word :=
+#[global] Instance IsRiscvMachine: RiscvProgram (StateAbortFail State) word :=
   AddExecTrace FieldNames (MinimalCSRsDet.IsRiscvMachine FieldNames).
 
 (* success flag * final state *)
diff --git a/src/riscv/Examples/SMTVerif.v b/src/riscv/Examples/SMTVerif.v
index 8058dba..3ddfc3f 100644
--- a/src/riscv/Examples/SMTVerif.v
+++ b/src/riscv/Examples/SMTVerif.v
@@ -59,7 +59,7 @@ Definition loadN(n: nat)(kind: SourceType)(a: word): OState MachineState (HList.
 Definition storeN(n: nat)(kind: SourceType)(a: word)(v: HList.tuple byte n): OState MachineState unit :=
   fail_hard.
 
-Instance IsRiscvProgram: RiscvProgram (OState MachineState) word :=  {
+#[global] Instance IsRiscvProgram: RiscvProgram (OState MachineState) word :=  {
   getRegister reg :=
     if Z.eq_dec reg Register0 then
       Return (ZToReg 0)
diff --git a/src/riscv/Examples/WMMFree.v b/src/riscv/Examples/WMMFree.v
index fbd82b7..0f3ca69 100644
--- a/src/riscv/Examples/WMMFree.v
+++ b/src/riscv/Examples/WMMFree.v
@@ -278,7 +278,7 @@ Fixpoint bind{A B: Type}(m: M A){struct m}: (A -> M B) -> M B :=
   | HaltThread => fun f => HaltThread (* Note: Drops the continuation in f *)
   end.
 
-Instance M_Monad: Monad M. refine ({|
+#[global] Instance M_Monad: Monad M. refine ({|
   Bind := @bind;
   Return := @Ret
 |}).
@@ -471,7 +471,7 @@ Definition updateDeps(inst: Instruction): Array Register (set Event) -> Array Re
   | _ => id (* only I is supported at the moment *)
   end.
 
-Instance IsRiscvMachine: RiscvProgram M word :=  {
+#[global] Instance IsRiscvMachine: RiscvProgram M word :=  {
   getRegister reg := s <- get; Return (getReg s.(Regs) reg);
   setRegister reg v := s <- get; put (withRegs (setReg s.(Regs) reg v) s);
   getPC := s <- get; Return s.(Pc);
diff --git a/src/riscv/Platform/AtomicMinimal.v b/src/riscv/Platform/AtomicMinimal.v
index 5170483..3c3f246 100644
--- a/src/riscv/Platform/AtomicMinimal.v
+++ b/src/riscv/Platform/AtomicMinimal.v
@@ -73,4 +73,4 @@ Section Riscv.
 
 End Riscv.
 
-Existing Instance IsAtomicRiscvMachine.
+#[global] Existing Instance IsAtomicRiscvMachine.
diff --git a/src/riscv/Platform/FE310ExtSpec.v b/src/riscv/Platform/FE310ExtSpec.v
index ce32111..6db8245 100644
--- a/src/riscv/Platform/FE310ExtSpec.v
+++ b/src/riscv/Platform/FE310ExtSpec.v
@@ -24,4 +24,4 @@ Section MMIO.
 
 End MMIO.
 
-Hint Resolve FE310_mmio: typeclass_instances.
+#[global] Hint Resolve FE310_mmio: typeclass_instances.
diff --git a/src/riscv/Platform/MetricLogging.v b/src/riscv/Platform/MetricLogging.v
index c2517cc..07956c5 100644
--- a/src/riscv/Platform/MetricLogging.v
+++ b/src/riscv/Platform/MetricLogging.v
@@ -59,7 +59,7 @@ Delimit Scope MetricL_scope with metricsL.
 Infix "<=" := metricsLeq : MetricL_scope.
 Infix "-" := metricsSub : MetricL_scope.
 
-Hint Unfold
+#[global] Hint Unfold
      withInstructions
      withLoads
      withStores
diff --git a/src/riscv/Platform/MetricMinimal.v b/src/riscv/Platform/MetricMinimal.v
index 4c795ed..6c1b83b 100644
--- a/src/riscv/Platform/MetricMinimal.v
+++ b/src/riscv/Platform/MetricMinimal.v
@@ -151,4 +151,4 @@ Section Riscv.
 
 End Riscv.
 
-Existing Instance IsMetricRiscvMachine.
+#[global] Existing Instance IsMetricRiscvMachine.
diff --git a/src/riscv/Platform/Minimal.v b/src/riscv/Platform/Minimal.v
index b198fa6..a2da920 100644
--- a/src/riscv/Platform/Minimal.v
+++ b/src/riscv/Platform/Minimal.v
@@ -260,5 +260,5 @@ Section Riscv.
 End Riscv.
 
 (* needed because defined inside a Section *)
-Existing Instance IsRiscvMachine.
-Existing Instance MinimalSatisfiesPrimitives.
+#[global] Existing Instance IsRiscvMachine.
+#[global] Existing Instance MinimalSatisfiesPrimitives.
diff --git a/src/riscv/Platform/MinimalCSRsDet.v b/src/riscv/Platform/MinimalCSRsDet.v
index c881b97..d63e163 100644
--- a/src/riscv/Platform/MinimalCSRsDet.v
+++ b/src/riscv/Platform/MinimalCSRsDet.v
@@ -120,4 +120,4 @@ Section Riscv.
 End Riscv.
 
 (* needed because defined inside a Section *)
-Existing Instance IsRiscvMachine.
+#[global] Existing Instance IsRiscvMachine.
diff --git a/src/riscv/Platform/MinimalLogging.v b/src/riscv/Platform/MinimalLogging.v
index 267c9af..7e40327 100644
--- a/src/riscv/Platform/MinimalLogging.v
+++ b/src/riscv/Platform/MinimalLogging.v
@@ -77,4 +77,4 @@ Section Riscv.
 
 End Riscv.
 
-Existing Instance IsRiscvMachineL. (* needed because it was defined inside a Section *)
+#[global] Existing Instance IsRiscvMachineL. (* needed because it was defined inside a Section *)
diff --git a/src/riscv/Proofs/EncodeBound.v b/src/riscv/Proofs/EncodeBound.v
index 476157d..252fb78 100644
--- a/src/riscv/Proofs/EncodeBound.v
+++ b/src/riscv/Proofs/EncodeBound.v
@@ -68,7 +68,7 @@ Lemma encode_U_bitSlice_idemp: forall opcode r z,
               encode_U opcode r z.
 Proof. intros. unfold encode_U. prove_Zeq_bitwise. Qed.
 
-Hint Rewrite
+#[global] Hint Rewrite
   encode_Fence_bitSlice_idemp
   encode_Invalid_bitSlice_idemp
   encode_I_bitSlice_idemp
diff --git a/src/riscv/Spec/CSRFile.v b/src/riscv/Spec/CSRFile.v
index 8c44cd8..5bda6eb 100644
--- a/src/riscv/Spec/CSRFile.v
+++ b/src/riscv/Spec/CSRFile.v
@@ -87,7 +87,7 @@ Proof. intros. destruct f1; destruct f2; simpl in *; congruence. Qed.
 
 Definition CSRField_ltb(f1 f2: CSRField): bool := Z.ltb (CSRField_to_Z f1) (CSRField_to_Z f2).
 
-Instance CSRField_ltb_strictorder: SortedList.parameters.strict_order CSRField_ltb.
+#[global] Instance CSRField_ltb_strictorder: SortedList.parameters.strict_order CSRField_ltb.
 Proof.
   constructor; unfold CSRField_ltb; intros.
   - apply Z.ltb_irrefl.
@@ -97,14 +97,14 @@ Proof.
     blia.
 Qed.
 
-Instance CSRFile_map_params: SortedList.parameters := {|
+#[global] Instance CSRFile_map_params: SortedList.parameters := {|
   parameters.key := CSRField;
   parameters.value := MachineInt;
   parameters.ltb := CSRField_ltb;
 |}.
 
-Instance CSRFile: map.map CSRField MachineInt :=
+#[global] Instance CSRFile: map.map CSRField MachineInt :=
   SortedList.map CSRFile_map_params CSRField_ltb_strictorder.
 
-Instance CSRFile_ok: map.ok CSRFile.
+#[global] Instance CSRFile_ok: map.ok CSRFile.
 Proof. apply (@SortedList.map_ok CSRFile_map_params CSRField_ltb_strictorder). Qed.
diff --git a/src/riscv/Spec/Machine.v b/src/riscv/Spec/Machine.v
index dd7c472..5a3a86f 100644
--- a/src/riscv/Spec/Machine.v
+++ b/src/riscv/Spec/Machine.v
@@ -147,4 +147,4 @@ Arguments RiscvProgram (M) (t) {_} {_}.
 Arguments RiscvMachine: clear implicits.
 Arguments RiscvMachine (M) (t) {_} {_} {_}.
 
-Existing Instance DefaultRiscvState.
+#[global] Existing Instance DefaultRiscvState.
diff --git a/src/riscv/Utility/DefaultMemImpl32.v b/src/riscv/Utility/DefaultMemImpl32.v
index 73c0447..dba412d 100644
--- a/src/riscv/Utility/DefaultMemImpl32.v
+++ b/src/riscv/Utility/DefaultMemImpl32.v
@@ -6,11 +6,11 @@ Require Import riscv.Utility.Words32Naive.
 Require coqutil.Map.SortedList coqutil.Map.SortedListWord.
 
 
-Instance params: SortedList.parameters := {|
+#[global] Instance params: SortedList.parameters := {|
   SortedList.parameters.key := word32;
   SortedList.parameters.value := Byte.byte;
   SortedList.parameters.ltb := word.ltu;
 |}.
 
-Instance Mem: map.map word32 Byte.byte := SortedList.map params _.
-Instance MemOk: map.ok Mem := SortedList.map_ok.
+#[global] Instance Mem: map.map word32 Byte.byte := SortedList.map params _.
+#[global] Instance MemOk: map.ok Mem := SortedList.map_ok.
diff --git a/src/riscv/Utility/DefaultMemImpl64.v b/src/riscv/Utility/DefaultMemImpl64.v
index 7aa5481..5b07c39 100644
--- a/src/riscv/Utility/DefaultMemImpl64.v
+++ b/src/riscv/Utility/DefaultMemImpl64.v
@@ -6,11 +6,11 @@ Require Import riscv.Utility.Words64Naive.
 Require coqutil.Map.SortedList coqutil.Map.SortedListWord.
 
 
-Instance params: SortedList.parameters := {|
+#[global] Instance params: SortedList.parameters := {|
   SortedList.parameters.key := word64;
   SortedList.parameters.value := Byte.byte;
   SortedList.parameters.ltb := word.ltu;
 |}.
 
-Instance Mem: map.map word64 Byte.byte := SortedList.map params _.
-Instance MemOk: map.ok Mem := SortedList.map_ok.
+#[global] Instance Mem: map.map word64 Byte.byte := SortedList.map params _.
+#[global] Instance MemOk: map.ok Mem := SortedList.map_ok.
diff --git a/src/riscv/Utility/Encode.v b/src/riscv/Utility/Encode.v
index 64c114e..0634d48 100644
--- a/src/riscv/Utility/Encode.v
+++ b/src/riscv/Utility/Encode.v
@@ -418,7 +418,7 @@ Definition verify_iset(inst: Instruction)(iset: InstructionSet): Prop :=
 Definition verify(inst: Instruction)(iset: InstructionSet): Prop :=
   respects_bounds (bitwidth iset) inst /\ verify_iset inst iset.
 
-Hint Unfold
+#[global] Hint Unfold
   map_Invalid
   map_R
   map_R_atomic
diff --git a/src/riscv/Utility/JMonad.v b/src/riscv/Utility/JMonad.v
index 156b2fa..d576d11 100644
--- a/src/riscv/Utility/JMonad.v
+++ b/src/riscv/Utility/JMonad.v
@@ -21,7 +21,7 @@ Open Scope monad_scope.
 
 Definition Id: Type -> Type := id.
 
-Instance Id_monad: Monad Id := {|
+#[global] Instance Id_monad: Monad Id := {|
   ret := @id;
   mmap A B := @id (A -> B);
   join := @id;
@@ -48,7 +48,7 @@ Definition flattenOption{A}(ooa: option (option A)): option A :=
   | _ => None
   end.
 
-Instance OptionT_Monad(M: Type -> Type){MM: Monad M}: Monad (optionT M) := {|
+#[global] Instance OptionT_Monad(M: Type -> Type){MM: Monad M}: Monad (optionT M) := {|
   ret A (a: A) := mkOptionT (ret (retOption a));
   mmap A B (f: A -> B)(oma: optionT M A) :=
     mkOptionT (mmap (mapOption f)
@@ -75,7 +75,7 @@ Record listT(M: Type -> Type)(A: Type): Type := mkListT {
 Arguments mkListT {M} {A} (_).
 Arguments runListT {M} {A} (_).
 
-Instance listT_Monad(M: Type -> Type){MM: Monad M}: Monad (listT M) := {|
+#[global] Instance listT_Monad(M: Type -> Type){MM: Monad M}: Monad (listT M) := {|
   ret A (a: A) := mkListT (ret (retList a));
   mmap A B (f: A -> B)(nma: listT M A) :=
     mkListT (mmap (mapList f)
@@ -98,7 +98,7 @@ Record StateT(S: Type)(M: Type -> Type)(A: Type): Type := mkStateT {
 Arguments mkStateT {S} {M} {A} (_).
 Arguments runStateT {S} {M} {A} (_).
 
-Instance StateT_Monad(S: Type)(M: Type -> Type){MM: Monad M}: Monad (StateT S M) := {|
+#[global] Instance StateT_Monad(S: Type)(M: Type -> Type){MM: Monad M}: Monad (StateT S M) := {|
   ret A (a: A) := mkStateT (fun s => ret (a, s));
   mmap A B (f: A -> B)(sma: StateT S M A) :=
     mkStateT (fun s => mmap (fun '(a, s0) => (f a, s0)) (runStateT sma s));
@@ -171,7 +171,7 @@ Instance NDStateT_Monad(S: Type)(M: Type -> Type){MM: Monad M}: Monad (NDStateT
 *)
 
 (* note: no "pick" is needed as argument here *)
-Instance NDS_Monad(S: Type): Monad (NDS S) := {|
+#[global] Instance NDS_Monad(S: Type): Monad (NDS S) := {|
   ret A (a: A) :=
     fun s => cons (a, s) nil;
   mmap A B (f: A -> B)(m: NDS S A) :=
diff --git a/src/riscv/Utility/MkMachineWidth.v b/src/riscv/Utility/MkMachineWidth.v
index ad9d3ba..73eb3d5 100644
--- a/src/riscv/Utility/MkMachineWidth.v
+++ b/src/riscv/Utility/MkMachineWidth.v
@@ -6,7 +6,7 @@ Require Import coqutil.Datatypes.HList.
 Require Import riscv.Utility.Utility.
 Local Open Scope Z_scope.
 
-Instance MachineWidth_XLEN{width}{_: Bitwidth width}{word: word width}: MachineWidth word := {|
+#[global] Instance MachineWidth_XLEN{width}{_: Bitwidth width}{word: word width}: MachineWidth word := {|
   add := word.add;
   sub := word.sub;
   mul := word.mul;
diff --git a/src/riscv/Utility/MonadT.v b/src/riscv/Utility/MonadT.v
index 794d5e3..5714f16 100644
--- a/src/riscv/Utility/MonadT.v
+++ b/src/riscv/Utility/MonadT.v
@@ -21,7 +21,7 @@ Notation "m1 ;; m2" := (Bind m1 (fun _ => m2))
 
 Open Scope monad_scope.
 
-Instance option_Monad: Monad option := {|
+#[global] Instance option_Monad: Monad option := {|
   Bind := fun {A B: Type} (o: option A) (f: A -> option B) => match o with
             | Some x => f x
             | None => None
@@ -75,7 +75,7 @@ listT option nat
 (*Eval cbv in (optionT list nat).*)
 
 
-Instance OptionT_Monad(M: Type -> Type){MM: Monad M}: Monad (optionT M) := {|
+#[global] Instance OptionT_Monad(M: Type -> Type){MM: Monad M}: Monad (optionT M) := {|
   Bind{A}{B}(m: M (option A))(f: A -> M (option B)) :=
     Bind m (fun (o: option A) =>
               match o with
@@ -98,7 +98,7 @@ End OptionMonad.
 
 Definition State(S A: Type) := S -> (A * S).
 
-Instance State_Monad(S: Type): Monad (State S) := {|
+#[global] Instance State_Monad(S: Type): Monad (State S) := {|
   Bind := fun {A B: Type} (m: State S A) (f: A -> State S B) =>
               fun (s: S) => let (a, s') := m s in f a s' ;
   Return := fun {A: Type} (a: A) =>
@@ -107,7 +107,7 @@ Instance State_Monad(S: Type): Monad (State S) := {|
 
 Definition StateT(S: Type)(M: Type -> Type)(A: Type) := S -> M (A * S)%type.
 
-Instance StateT_Monad(M: Type -> Type){MM: Monad M}(S: Type): Monad (StateT S M) := {|
+#[global] Instance StateT_Monad(M: Type -> Type){MM: Monad M}(S: Type): Monad (StateT S M) := {|
   Bind{A B: Type}(m: StateT S M A)(f: A -> StateT S M B) :=
     fun (s: S) => Bind (m s) (fun '(a, s) => f a s);
   Return{A: Type}(a: A) :=
@@ -174,7 +174,7 @@ Module NonDetMonad.
 
 End NonDetMonad.
 
-Instance NonDet_Monad: Monad NonDet := {|
+#[global] Instance NonDet_Monad: Monad NonDet := {|
   Bind := @NonDetMonad.flatMapSet;
   Return := @NonDetMonad.singletonSet;
 |}.
@@ -184,7 +184,7 @@ Definition NonDetT(M: Type -> Type)(A: Type) := NonDet (M A).
 Goal forall (M: Type -> Type) (A: Type), NonDet (M A) = (M A -> Prop).
   intros. reflexivity. Qed.
 
-Instance NonDetT_Monad(M: Type -> Type){MM: Monad M}: Monad (NonDetT M). refine ({|
+#[global] Instance NonDetT_Monad(M: Type -> Type){MM: Monad M}: Monad (NonDetT M). refine ({|
   Bind{A B}(m: NonDet (M A))(f: A -> NonDet (M B)) := _;
   Return := _
 |}).
diff --git a/src/riscv/Utility/MonadTests.v b/src/riscv/Utility/MonadTests.v
index 9255b83..b2efbf1 100644
--- a/src/riscv/Utility/MonadTests.v
+++ b/src/riscv/Utility/MonadTests.v
@@ -17,7 +17,7 @@ Open Scope monad_scope.
 
 Definition Id: Type -> Type := id.
 
-Instance Id_monad: Monad Id := {|
+#[global] Instance Id_monad: Monad Id := {|
   Bind{A B}(m: A)(f: A -> B) := f m;
   Return{A}(a: A) := a;
 |}.
@@ -25,7 +25,7 @@ Instance Id_monad: Monad Id := {|
 
 Definition NonDet(A: Type): Type := A -> Prop.
 
-Instance NonDet_Monad: Monad NonDet := {|
+#[global] Instance NonDet_Monad: Monad NonDet := {|
   Bind{A B}(m: NonDet A)(f: A -> NonDet B) :=
     fun (b: B) => exists a, m a /\ f a b;
   Return{A} := eq;
@@ -38,7 +38,7 @@ Record optionT(M: Type -> Type)(A: Type): Type := mkOptionT {
 Arguments mkOptionT {M} {A} (_).
 Arguments runOptionT {M} {A} (_).
 
-Instance OptionT_Monad(M: Type -> Type){MM: Monad M}: Monad (optionT M) := {|
+#[global] Instance OptionT_Monad(M: Type -> Type){MM: Monad M}: Monad (optionT M) := {|
   Bind{A}{B}(m: optionT M A)(f: A -> optionT M B) :=
     mkOptionT (Bind (runOptionT m) (fun (o: option A) =>
                                       match o with
@@ -63,7 +63,7 @@ Record StateT(S: Type)(M: Type -> Type)(A: Type): Type := mkStateT {
 Arguments mkStateT {S} {M} {A} (_).
 Arguments runStateT {S} {M} {A} (_).
 
-Instance StateT_Monad(M: Type -> Type){MM: Monad M}(S: Type): Monad (StateT S M) := {|
+#[global] Instance StateT_Monad(M: Type -> Type){MM: Monad M}(S: Type): Monad (StateT S M) := {|
   Bind{A B: Type}(m: StateT S M A)(f: A -> StateT S M B) :=
     mkStateT (fun (s: S) => Bind ((runStateT m) s) (fun '(a, s) => runStateT (f a) s));
   Return{A: Type}(a: A) :=
@@ -86,7 +86,7 @@ Record listT(M: Type -> Type)(A: Type): Type := mkListT {
 Arguments mkListT {M} {A} (_).
 Arguments runListT {M} {A} (_).
 
-Instance listT_Monad(M: Type -> Type){MM: Monad M}: Monad (listT M) := {|
+#[global] Instance listT_Monad(M: Type -> Type){MM: Monad M}: Monad (listT M) := {|
   Bind{A B: Type}(m: listT M A)(f: A -> listT M B) :=
     mkListT (la <- runListT m;
              List.fold_left
diff --git a/src/riscv/Utility/Monads.v b/src/riscv/Utility/Monads.v
index 5a3c24e..a4ebc17 100644
--- a/src/riscv/Utility/Monads.v
+++ b/src/riscv/Utility/Monads.v
@@ -37,7 +37,7 @@ Ltac prove_monad_law :=
          | o: option _ |- _ => destruct o
          end.
 
-Instance option_Monad: Monad option. refine ({|
+#[global] Instance option_Monad: Monad option. refine ({|
   Bind A B (o: option A) (f: A -> option B) :=
     match o with
     | Some x => f x
@@ -51,7 +51,7 @@ Defined.
 
 Definition NonDet(A: Type): Type := A -> Prop.
 
-Instance NonDet_Monad: Monad NonDet. refine ({|
+#[global] Instance NonDet_Monad: Monad NonDet. refine ({|
   Bind A B (m: NonDet A)(f: A -> NonDet B) :=
     fun (b: B) => exists a, m a /\ f a b;
   Return A := eq;
@@ -62,7 +62,7 @@ Defined.
 
 Definition State(S A: Type) := S -> (A * S).
 
-Instance State_Monad(S: Type): Monad (State S). refine ({|
+#[global] Instance State_Monad(S: Type): Monad (State S). refine ({|
   Bind A B (m: State S A) (f: A -> State S B) :=
     fun (s: S) => let (a, s') := m s in f a s' ;
   Return A (a: A) :=
@@ -80,7 +80,7 @@ End StateOperations.
 
 Definition OState(S A: Type) := S -> (option A) * S.
 
-Instance OState_Monad(S: Type): Monad (OState S). refine ({|
+#[global] Instance OState_Monad(S: Type): Monad (OState S). refine ({|
   Bind A B (m: OState S A) (f: A -> OState S B) :=
     fun (s: S) => match m s with
                   | (Some a, s') => f a s'
@@ -100,7 +100,7 @@ Module OStateOperations.
   Definition fail_hard{S A: Type}: OState S A :=
     fun (s: S) => (None, s).
 
-  Hint Unfold get put fail_hard : unf_monad_ops.
+  #[global] Hint Unfold get put fail_hard : unf_monad_ops.
 
   Lemma Bind_get{S A: Type}: forall (f: S -> OState S A) (s: S),
       Bind get f s = f s s.
@@ -194,7 +194,7 @@ End OStateOperations.
    a unique set of all possible outcomes. *)
 Definition StateND(S A: Type) := S -> (A * S) -> Prop.
 
-Instance StateND_Monad(S: Type): Monad (StateND S). refine ({|
+#[global] Instance StateND_Monad(S: Type): Monad (StateND S). refine ({|
   Bind A B (m: StateND S A)(f : A -> StateND S B) :=
     fun (s1 : S) bs3 => exists a s2, m s1 (a, s2) /\ f a s2 bs3;
   Return A (a : A) :=
@@ -217,7 +217,7 @@ Module StateNDOperations.
   Definition arbitrary{S: Type}(A: Type): StateND S A :=
     fun (s: S) (a_s: (A * S)) => exists a, a_s = (a, s).
 
-  Hint Unfold get put unspecified_behavior arbitrary : unf_monad_ops.
+  #[global] Hint Unfold get put unspecified_behavior arbitrary : unf_monad_ops.
 
   Lemma Bind_get{S A: Type}: forall (f: S -> StateND S A) (s: S),
       Bind get f s = f s s.
@@ -244,7 +244,7 @@ End StateNDOperations.
    a unique set of all possible outcomes. *)
 Definition OStateND(S A: Type) := S -> option (A * S) -> Prop.
 
-Instance OStateND_Monad(S: Type): Monad (OStateND S). refine ({|
+#[global] Instance OStateND_Monad(S: Type): Monad (OStateND S). refine ({|
   Bind A B (m: OStateND S A)(f : A -> OStateND S B) :=
     fun (s : S) (obs: option (B * S)) =>
       (m s None /\ obs = None) \/
@@ -269,7 +269,7 @@ Module OStateNDOperations.
   Definition arbitrary{S: Type}(A: Type): OStateND S A :=
     fun (s: S) (oas: option (A * S)) => exists a, oas = Some (a, s).
 
-  Hint Unfold get put fail_hard arbitrary : unf_monad_ops.
+  #[global] Hint Unfold get put fail_hard arbitrary : unf_monad_ops.
 
   Lemma Bind_get{S A: Type}: forall (f: S -> OStateND S A) (s: S),
       Bind get f s = f s s.
@@ -375,7 +375,7 @@ End OStateNDOperations.
    will return an answer and a final state that satisfy post. *)
 Definition Post(S A: Type) := S -> (A -> S -> Prop) -> Prop.
 
-Instance Post_Monad(S: Type): Monad (Post S). refine ({|
+#[global] Instance Post_Monad(S: Type): Monad (Post S). refine ({|
   Bind A B (m: Post S A) (f : A -> Post S B) :=
     fun s1 post => m s1 (fun a s2 => f a s2 post);
   Return A (a : A) :=
@@ -402,7 +402,7 @@ End PostMonadOperations.
 (* outer option is for failure, inner option is for early return (abort) *)
 Definition StateAbortFail(S A: Type) := S -> (option (option A) * S).
 
-Instance StateAbortFail_Monad(S: Type): Monad (StateAbortFail S). refine ({|
+#[global] Instance StateAbortFail_Monad(S: Type): Monad (StateAbortFail S). refine ({|
   Bind A B (m: StateAbortFail S A) (f: A -> StateAbortFail S B) (s1 : S) :=
     match m s1 with
     | (Some (Some a), s2) => f a s2
diff --git a/src/riscv/Utility/Words32Naive.v b/src/riscv/Utility/Words32Naive.v
index 00dd8e7..cd4d1d8 100644
--- a/src/riscv/Utility/Words32Naive.v
+++ b/src/riscv/Utility/Words32Naive.v
@@ -6,8 +6,8 @@ Require Import coqutil.Word.Naive.
 
 Local Open Scope Z_scope.
 
-Instance word: word.word 32 := Naive.word 32.
+#[global] Instance word: word.word 32 := Naive.word 32.
 
-Instance Words32Naive: Bitwidth 32 := {|
+#[global] Instance Words32Naive: Bitwidth 32 := {|
   width_cases := or_introl eq_refl;
 |}.
diff --git a/src/riscv/Utility/Words64Naive.v b/src/riscv/Utility/Words64Naive.v
index c7039d6..a90b4fa 100644
--- a/src/riscv/Utility/Words64Naive.v
+++ b/src/riscv/Utility/Words64Naive.v
@@ -6,8 +6,8 @@ Require Import coqutil.Word.Bitwidth.
 
 Local Open Scope Z_scope.
 
-Instance word: word.word 64 := Naive.word 64.
+#[global] Instance word: word.word 64 := Naive.word 64.
 
-Instance Words64Naive: Bitwidth 64 := {|
+#[global] Instance Words64Naive: Bitwidth 64 := {|
   width_cases := or_intror eq_refl;
 |}.