Qualify `Instance` and `Program Instance` as `Global`

This avoids a new warning of Coq 8.14.

15 files changed, 53 insertions, 53 deletions

diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v
index b2a2308e..704c392e 100644
--- a/aarch64/Machregs.v
+++ b/aarch64/Machregs.v
@@ -54,9 +54,9 @@ Proof.
   intros. specialize (H r). InvBooleans. auto.
 Qed.
 
-Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
+Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
 
-Instance Finite_mreg : Finite mreg := {
+Global Instance Finite_mreg : Finite mreg := {
   Finite_elements := all_mregs;
   Finite_elements_spec := all_mregs_complete
 }.
diff --git a/arm/Machregs.v b/arm/Machregs.v
index ae0ff6bf..dd365555 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -57,9 +57,9 @@ Proof.
   intros. specialize (H r). InvBooleans. auto.
 Qed.
 
-Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
+Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
 
-Instance Finite_mreg : Finite mreg := {
+Global Instance Finite_mreg : Finite mreg := {
   Finite_elements := all_mregs;
   Finite_elements_spec := all_mregs_complete
 }.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 4755ab79..d66c7de8 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -1463,7 +1463,7 @@ End PRESERVATION.
 
 (** ** Commutation with linking *)
 
-Instance TransfSelectionLink : TransfLink match_prog.
+Global Instance TransfSelectionLink : TransfLink match_prog.
 Proof.
   red; intros. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
   eapply link_match_program; eauto.
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 3216ec50..fec3c9f8 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -1435,4 +1435,4 @@ Proof.
 * intros. apply PTree.elements_keys_norepet.
 Qed.
 
-Instance TransfSelectionLink : TransfLink match_prog := link_match_program.
+Global Instance TransfSelectionLink : TransfLink match_prog := link_match_program.
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 8e396e2a..98293888 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -1968,7 +1968,7 @@ End CORRECTNESS.
 
 (** ** Commutation with linking *)
 
-Instance TransfCshmgenLink : TransfLink match_prog.
+Global Instance TransfCshmgenLink : TransfLink match_prog.
 Proof.
   red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2).
   generalize H.
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index e3356510..504e8be1 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -1530,7 +1530,7 @@ Unset Implicit Arguments.
 
 (** ** Linking types *)
 
-Program Instance Linker_types : Linker type := {
+Global Program Instance Linker_types : Linker type := {
   link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None;
   linkorder := fun t1 t2 => t1 = t2
 }.
@@ -1579,7 +1579,7 @@ Proof.
   assert (x = y) by eauto. subst y. auto.
 Qed.
 
-Program Instance Linker_composite_defs : Linker (list composite_definition) := {
+Global Program Instance Linker_composite_defs : Linker (list composite_definition) := {
   link := link_composite_defs;
   linkorder := @List.incl composite_definition
 }.
@@ -1765,7 +1765,7 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
   | linkorder_fundef_ext_int: forall f id sg targs tres cc,
       linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f).
 
-Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
+Global Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
   link := link_fundef;
   linkorder := linkorder_fundef
 }.
@@ -1828,7 +1828,7 @@ Definition linkorder_program {F: Type} (p1 p2: program F) : Prop :=
      linkorder (program_of_program p1) (program_of_program p2)
   /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co).
 
-Program Instance Linker_program (F: Type): Linker (program F) := {
+Global Program Instance Linker_program (F: Type): Linker (program F) := {
   link := link_program;
   linkorder := linkorder_program
 }.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 67bf0e51..507e2128 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -2444,7 +2444,7 @@ End PRESERVATION.
 
 (** ** Commutation with linking *)
 
-Instance TransfSimplExprLink : TransfLink match_prog.
+Global Instance TransfSimplExprLink : TransfLink match_prog.
 Proof.
   red; intros. eapply Ctypes.link_match_program_gen; eauto. 
 - intros.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index e4b759c4..c133d8ea 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -2320,7 +2320,7 @@ End PRESERVATION.
 
 (** ** Commutation with linking *)
 
-Instance TransfSimplLocalsLink : TransfLink match_prog.
+Global Instance TransfSimplLocalsLink : TransfLink match_prog.
 Proof.
   red; intros. eapply Ctypes.link_match_program; eauto. 
 - intros.
diff --git a/common/Linking.v b/common/Linking.v
index d23b1028..4ef83d42 100644
--- a/common/Linking.v
+++ b/common/Linking.v
@@ -60,7 +60,7 @@ Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
   | linkorder_fundef_refl: forall fd, linkorder_fundef fd fd
   | linkorder_fundef_ext_int: forall f id sg, linkorder_fundef (External (EF_external id sg)) (Internal f).
 
-Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
+Global Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
   link := link_fundef;
   linkorder := linkorder_fundef
 }.
@@ -114,7 +114,7 @@ Inductive linkorder_varinit: list init_data -> list init_data -> Prop :=
       il <> nil -> init_data_list_size il = sz ->
       linkorder_varinit (Init_space sz :: nil) il.
 
-Program Instance Linker_varinit : Linker (list init_data) := {
+Global Program Instance Linker_varinit : Linker (list init_data) := {
   link := link_varinit;
   linkorder := linkorder_varinit
 }.
@@ -163,7 +163,7 @@ Inductive linkorder_vardef {V: Type} {LV: Linker V}: globvar V -> globvar V -> P
       linkorder i1 i2 ->
       linkorder_vardef (mkglobvar info1 i1 ro vo) (mkglobvar info2 i2 ro vo).
 
-Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := {
+Global Program Instance Linker_vardef (V: Type) {LV: Linker V}: Linker (globvar V) := {
   link := link_vardef;
   linkorder := linkorder_vardef
 }.
@@ -189,7 +189,7 @@ Global Opaque Linker_vardef.
 
 (** A trivial linker for the trivial var info [unit]. *)
 
-Program Instance Linker_unit: Linker unit := {
+Global Program Instance Linker_unit: Linker unit := {
   link := fun x y => Some tt;
   linkorder := fun x y => True
 }.
@@ -215,7 +215,7 @@ Inductive linkorder_def {F V: Type} {LF: Linker F} {LV: Linker V}: globdef F V -
       linkorder v1 v2 ->
       linkorder_def (Gvar v1) (Gvar v2).
 
-Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := {
+Global Program Instance Linker_def (F V: Type) {LF: Linker F} {LV: Linker V}: Linker (globdef F V) := {
   link := link_def;
   linkorder := linkorder_def
 }.
@@ -332,7 +332,7 @@ Qed.
 
 End LINKER_PROG.
 
-Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := {
+Global Program Instance Linker_prog (F V: Type) {LF: Linker F} {LV: Linker V} : Linker (program F V) := {
   link := link_prog;
   linkorder := fun p1 p2 =>
      p1.(prog_main) = p2.(prog_main)
@@ -699,7 +699,7 @@ Local Transparent Linker_fundef.
 - destruct (external_function_eq ef1 ef2); inv H. exists (External ef2); split; auto. simpl. rewrite dec_eq_true; auto.
 Qed.
 
-Instance TransfPartialContextualLink
+Global Instance TransfPartialContextualLink
            {A B C V: Type} {LV: Linker V}
            (tr_fun: C -> A -> res B)
            (ctx_for: program (fundef A) V -> C):
@@ -714,7 +714,7 @@ Proof.
 - intros; subst. exists v; auto.
 Qed.
 
-Instance TransfPartialLink
+Global Instance TransfPartialLink
            {A B V: Type} {LV: Linker V}
            (tr_fun: A -> res B):
   TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) =>
@@ -728,7 +728,7 @@ Proof.
 - intros; subst. exists v; auto.
 Qed.
 
-Instance TransfTotallContextualLink
+Global Instance TransfTotallContextualLink
            {A B C V: Type} {LV: Linker V}
            (tr_fun: C -> A -> B)
            (ctx_for: program (fundef A) V -> C):
@@ -747,7 +747,7 @@ Proof.
 - intros; subst. exists v; auto.
 Qed.
 
-Instance TransfTotalLink
+Global Instance TransfTotalLink
            {A B V: Type} {LV: Linker V}
            (tr_fun: A -> B):
   TransfLink (fun (p1: program (fundef A) V) (p2: program (fundef B) V) =>
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 75247f71..b00d067e 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -209,7 +209,7 @@ Proof.
   intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence.
 Qed.
 
-Instance TransfIfLink {A: Type} {LA: Linker A}
+Global Instance TransfIfLink {A: Type} {LA: Linker A}
                       (flag: unit -> bool) (transf: A -> A -> Prop) (TL: TransfLink transf)
                       : TransfLink (match_if flag transf).
 Proof.
diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v
index 69ba4723..224c9640 100644
--- a/lib/Decidableplus.v
+++ b/lib/Decidableplus.v
@@ -27,14 +27,14 @@ Ltac decide_goal := eapply Decidable_sound; reflexivity.
 
 (** Deciding logical connectives *)
 
-Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := {
+Global Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := {
   Decidable_witness := negb (@Decidable_witness P dP)
 }.
 Next Obligation.
   rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt.
 Qed.
 
-Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := {
+Global Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := {
   Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ)
 }.
 Next Obligation.
@@ -46,21 +46,21 @@ Next Obligation.
   eapply Decidable_sound_alt; rewrite H; eapply Decidable_complete_alt; eauto.
 Qed.
 
-Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := {
+Global Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := {
   Decidable_witness := @Decidable_witness P dP && @Decidable_witness Q dQ
 }.
 Next Obligation.
   rewrite andb_true_iff. rewrite ! Decidable_spec. tauto.
 Qed.
 
-Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := {
+Global Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := {
   Decidable_witness := @Decidable_witness P dP || @Decidable_witness Q dQ
 }.
 Next Obligation.
   rewrite orb_true_iff. rewrite ! Decidable_spec. tauto.
 Qed.
 
-Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := {
+Global Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := {
   Decidable_witness := if @Decidable_witness P dP then @Decidable_witness Q dQ else true
 }.
 Next Obligation.
@@ -79,28 +79,28 @@ Next Obligation.
   split; intros. InvBooleans. auto. subst y. apply dec_eq_true.
 Qed.
 
-Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
+Global Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
   Decidable_witness := Bool.eqb x y
 }.
 Next Obligation.
   apply eqb_true_iff.
 Qed.
 
-Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
+Global Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
   Decidable_witness := Nat.eqb x y
 }.
 Next Obligation.
   apply Nat.eqb_eq.
 Qed.
 
-Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := {
+Global Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := {
   Decidable_witness := Pos.eqb x y
 }.
 Next Obligation.
   apply Pos.eqb_eq.
 Qed.
 
-Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
+Global Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
   Decidable_witness := Z.eqb x y
 }.
 Next Obligation.
@@ -109,35 +109,35 @@ Qed.
 
 (** Deciding order on Z *)
 
-Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := {
+Global Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := {
   Decidable_witness := Z.leb x y
 }.
 Next Obligation.
   apply Z.leb_le.
 Qed.
 
-Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := {
+Global Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := {
   Decidable_witness := Z.ltb x y
 }.
 Next Obligation.
   apply Z.ltb_lt.
 Qed.
 
-Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := {
+Global Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := {
   Decidable_witness := Z.geb x y
 }.
 Next Obligation.
   rewrite Z.geb_le. intuition lia.
 Qed.
 
-Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := {
+Global Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := {
   Decidable_witness := Z.gtb x y
 }.
 Next Obligation.
   rewrite Z.gtb_lt. intuition lia.
 Qed.
 
-Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := {
+Global Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := {
   Decidable_witness := Z.eqb y ((y / x) * x)%Z
 }.
 Next Obligation.
@@ -153,7 +153,7 @@ Qed.
 
 (** Deciding properties over lists *)
 
-Program Instance Decidable_forall_in_list :
+Global Program Instance Decidable_forall_in_list :
       forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
       Decidable (forall x:A, In x l -> P x) := {
   Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l
@@ -164,7 +164,7 @@ Next Obligation.
 - eapply Decidable_complete; eauto.
 Qed.
 
-Program Instance Decidable_exists_in_list :
+Global Program Instance Decidable_exists_in_list :
       forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
       Decidable (exists x:A, In x l /\ P x) := {
   Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l
@@ -184,7 +184,7 @@ Class Finite (T: Type) := {
 
 (** Deciding forall and exists quantification over finite types. *)
 
-Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := {
+Global Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := {
   Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
 }.
 Next Obligation.
@@ -193,7 +193,7 @@ Next Obligation.
 - eapply Decidable_complete; eauto.
 Qed.
 
-Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := {
+Global Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := {
   Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
 }.
 Next Obligation.
@@ -204,21 +204,21 @@ Qed.
 
 (** Some examples of finite types. *)
 
-Program Instance Finite_bool : Finite bool := {
+Global Program Instance Finite_bool : Finite bool := {
   Finite_elements := false :: true :: nil
 }.
 Next Obligation.
   destruct x; auto.
 Qed.
 
-Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := {
+Global Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := {
   Finite_elements := list_prod (@Finite_elements A fA) (@Finite_elements B fB)
 }.
 Next Obligation.
   apply List.in_prod; eapply Finite_elements_spec.
 Qed.
 
-Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := {
+Global Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := {
   Finite_elements := None :: List.map (@Some A) (@Finite_elements A fA)
 }.
 Next Obligation.
diff --git a/lib/Maps.v b/lib/Maps.v
index 6bc6e14b..3f43d102 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -1604,7 +1604,7 @@ Proof.
   intros. transitivity a0; auto.
 Qed.
 
-Instance Equal_Equivalence : Equivalence Equal := {
+Global Instance Equal_Equivalence : Equivalence Equal := {
   Equivalence_Reflexive := Equal_refl;
   Equivalence_Symmetric := Equal_sym;
   Equivalence_Transitive := Equal_trans
@@ -1633,7 +1633,7 @@ Next Obligation.
   unfold equiv, complement in H0. congruence.
 Qed.
 
-Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec.
+Global Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec.
 
 End EXTENSIONAL_EQUALITY.
 
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 9967bbae..eeca880a 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -75,9 +75,9 @@ Proof.
   intros. specialize (H r). InvBooleans. auto.
 Qed.
 
-Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
+Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
 
-Instance Finite_mreg : Finite mreg := {
+Global Instance Finite_mreg : Finite mreg := {
   Finite_elements := all_mregs;
   Finite_elements_spec := all_mregs_complete
 }.
diff --git a/riscV/Machregs.v b/riscV/Machregs.v
index d469e594..89fa37b0 100644
--- a/riscV/Machregs.v
+++ b/riscV/Machregs.v
@@ -78,9 +78,9 @@ Proof.
   intros. specialize (H r). InvBooleans. auto.
 Qed.
 
-Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
+Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
   
-Instance Finite_mreg : Finite mreg := {
+Global Instance Finite_mreg : Finite mreg := {
   Finite_elements := all_mregs;
   Finite_elements_spec := all_mregs_complete
 }.
diff --git a/x86/Machregs.v b/x86/Machregs.v
index 6f3064b8..a440bffc 100644
--- a/x86/Machregs.v
+++ b/x86/Machregs.v
@@ -57,9 +57,9 @@ Proof.
   intros. specialize (H r). InvBooleans. auto.
 Qed.
 
-Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
+Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq.
 
-Instance Finite_mreg : Finite mreg := {
+Global Instance Finite_mreg : Finite mreg := {
   Finite_elements := all_mregs;
   Finite_elements_spec := all_mregs_complete
 }.