Merge pull request #30 from Alizter/hint-locality-error

Adapt w.r.t. coq/coq#16004

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 := [

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 *)

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)

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);

src/riscv/Platform/AtomicMinimal.v

@@ -73,4 +73,4 @@ Section Riscv.
 
 End Riscv.
 
-Existing Instance IsAtomicRiscvMachine.
+#[global] Existing Instance IsAtomicRiscvMachine.

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.

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

src/riscv/Platform/MetricMinimal.v

@@ -151,4 +151,4 @@ Section Riscv.
 
 End Riscv.
 
-Existing Instance IsMetricRiscvMachine.
+#[global] Existing Instance IsMetricRiscvMachine.

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.

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.

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 *)

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

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.

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.

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.

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.

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

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) :=

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;

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 := _
 |}).

src/riscv/Utility/MonadTests.v

@@ -17,15 +17,15 @@ 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;
 |}.
 
 
 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