Merge pull request #415 from AbsInt/coq-8.14-compat

Improved compatibility with Coq 8.14

18 files changed, 68 insertions, 58 deletions

diff --git a/Makefile b/Makefile
index 4a9f3772..2bc39c33 100644
--- a/Makefile
+++ b/Makefile
@@ -53,11 +53,21 @@ endif
 # deprecated-ident-entry:
 #    warning introduced in 8.13
 #    suggested change (use `name` instead of `ident`) supported since 8.13
+# deprecated-hint-rewrite-without-locality:
+#    warning introduced in 8.14
+#    suggested change (add Global or Local or [#export] modifier)
+#    is not supported in 8.13 nor in 8.11, but was supported in 8.9 (go figure)
+# deprecated-instance-without-locality:
+#    warning introduced in 8.14
+#    triggered by Menhir-generated files, to be solved upstream in Menhir
 
 COQCOPTS ?= \
   -w -undeclared-scope \
   -w -unused-pattern-matching-variable \
-  -w -deprecated-ident-entry
+  -w -deprecated-ident-entry \
+  -w -deprecated-hint-rewrite-without-locality
+
+cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
 
 COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
 COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
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/configure b/configure
index 10f60262..1b224319 100755
--- a/configure
+++ b/configure
@@ -504,19 +504,19 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
-  8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2)
+  8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0|8.11.1|8.11.2|8.12.0|8.12.1|8.12.2|8.13.0|8.13.1|8.13.2|8.14.0)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.13.2"
+            echo "Error: CompCert requires a version of Coq between 8.9.0 and 8.14.0"
             missingtools=true
         fi;;
   "")
         echo "NOT FOUND"
-        echo "Error: make sure Coq version 8.12.2 is installed."
+        echo "Error: make sure Coq version 8.13.2 is installed."
         missingtools=true;;
 esac
 
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/flocq/IEEE754/Bits.v b/flocq/IEEE754/Bits.v
index 3c19e31b..b38d4900 100644
--- a/flocq/IEEE754/Bits.v
+++ b/flocq/IEEE754/Bits.v
@@ -181,7 +181,7 @@ cut (x / (2^mw * 2^ew) < 2)%Z. clear ; lia.
 apply Zdiv_lt_upper_bound.
 now apply Zmult_lt_0_compat.
 rewrite <- Zpower_exp ; try ( apply Z.le_ge ; apply Zlt_le_weak ; assumption ).
-change 2%Z at 1 with (Zpower 2 1).
+change 2%Z with (Zpower 2 1) at 1.
 rewrite <- Zpower_exp.
 now rewrite Zplus_comm.
 discriminate.
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
 }.