Merge remote-tracking branch 'origin/master' into towards_3.10

22 files changed, 103 insertions, 82 deletions

diff --git a/Makefile b/Makefile
index a5d56fee..c9bf9ed4 100644
--- a/Makefile
+++ b/Makefile
@@ -61,11 +61,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 bfe23e83..454a7cbe 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 1ec8f0a1..9fe8548b 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 e737ba4b..fe286627 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -1467,7 +1467,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 aaacf9d1..476208b0 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -1465,4 +1465,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 e373d4e5..d8653544 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -1974,7 +1974,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 76c46343..8d0555c6 100755
--- a/configure
+++ b/configure
@@ -352,7 +352,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         cc_options="-m64"
         casm_options="-m64 -c"
         clinker_options="-m64"
-        cprepro_options="-std=c99 -m64 -U__GNUC__ -E"
+        cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="bsd"
         ;;
     linux)
@@ -360,7 +360,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         cc_options="-m64"
         casm_options="-m64 -c"
         clinker_options="-m64"
-        cprepro_options="-std=c99 -m64 -U__GNUC__ -E"
+        cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="linux"
         ;;
     macos|macosx)
@@ -369,7 +369,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         casm_options="-arch x86_64 -c"
         clinker_options="-arch x86_64"
         clinker_needs_no_pie=false
-        cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
+        cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__SIZEOF_INT128__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
         libmath=""
         system="macos"
         ;;
@@ -378,7 +378,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         cc_options="-m64"
         casm_options="-m64 -c"
         clinker_options="-m64"
-        cprepro_options="-std=c99 -m64 -U__GNUC__ '-D__attribute__(x)=' -E"
+        cprepro_options="-std=c99 -m64 -U__GNUC__ -U__SIZEOF_INT128__ '-D__attribute__(x)=' -E"
         system="cygwin"
         ;;
     *)
@@ -541,19 +541,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.vexpand b/driver/Compiler.vexpand
index 9673267d..7503d3ed 100644
--- a/driver/Compiler.vexpand
+++ b/driver/Compiler.vexpand
@@ -163,7 +163,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 456a1a9a..c648af23 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -1761,7 +1761,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
@@ -1790,7 +1790,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/Asmgen.v b/powerpc/Asmgen.v
index 924773e7..eafb6d3c 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -183,7 +183,9 @@ Definition andimm64 (r1 r2: ireg) (n: int64) (k : code) :=
     andimm64_base r1 r2 n k.
 
 Definition rolm64 (r1 r2: ireg) (amount: int) (mask: int64) (k: code) :=
-  if is_rldl_mask mask || is_rldr_mask mask || is_rldl_mask (Int64.shru' mask amount) then
+  if is_rldl_mask mask || is_rldr_mask mask
+  || (let mask' := Int64.shru' mask amount in
+      Int64.eq mask (Int64.shl' mask' amount) && is_rldl_mask mask') then
     Prldinm r1 r2 amount mask :: k
   else
     Prldinm r1 r2 amount Int64.mone :: andimm64_base r1 r1 mask k.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index e25ae583..b6b5c678 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -294,10 +294,10 @@ Opaque Int.eq.
 - unfold xorimm64, opimm64. destruct Int64.eq. TailNoLabel.
   destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel.
 - unfold rolm64, andimm64_base, opimm64.
-  destruct (is_rldl_mask i0 || is_rldr_mask i0 || is_rldl_mask (Int64.shru' i0 i)). TailNoLabel.
-  apply tail_nolabel_cons; unfold nolabel; auto.
+  destruct orb.
+  TailNoLabel.
   destruct Int64.eq. TailNoLabel.
-  destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel.
+  destruct ireg_eq; TailNoLabel; eapply tail_nolabel_trans; TailNoLabel.
 - eapply transl_cond_op_label; eauto.
 - destruct (preg_of r); monadInv H. eapply transl_select_op_label; eauto. eapply transl_fselect_op_label; eauto.
 Qed.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index cc9fc1a7..c0651bf9 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -788,7 +788,7 @@ Lemma rolm64_correct:
   /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> important_preg r' = true  -> rs'#r' = rs#r'.
 Proof.
   intros. unfold rolm64.
-  destruct (is_rldl_mask mask || is_rldr_mask mask || is_rldl_mask (Int64.shru' mask amount)).
+  destruct orb.
 - econstructor; split. eapply exec_straight_one. simpl; reflexivity. reflexivity.
   intuition Simpl.
 - edestruct (andimm64_base_correct r1 r1 mask k) as (rs2 & A & B & C); auto.
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/powerpc/Op.v b/powerpc/Op.v
index 505b7545..0b379883 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -1367,53 +1367,62 @@ Definition is_rlw_mask (x: int) : bool :=
   is_mask_rec rlw_transition rlw_accepting Int.wordsize RLW_S0 (Int.unsigned x).
 
 (** For the 64-bit [rldicl] and [rldicr] instructions, the acceptable
-  masks are [1111100000] and [0000011111], that is, some ones in the
-  high bits and some zeroes in the low bits, or conversely.  All ones
-  is OK, but not all zeroes.  The corresponding automata are:
-<<
-      0          1
-     / \        / \
-     \ /        \ /          (accepting: [1])
-     [0] --1--> [1]
+  masks are (in big endian):
+- for [rldicl]: masks that clear the leftmost bits (most significant bits),
+  that is, [00000011111], that is, ones in the low bits followed by zeros
+  in the high bits;
+- for [rldicr]: masks that clear the rightmost bits (least significant bits),
+  that is, [11110000000], that is, zeros in the low bits followed by ones
+  in the high bits.
 
+  All ones  is OK, but not all zeroes.
 
+  The corresponding automata for [rldicl] is
+<<
                  1          0
                 / \        / \
                 \ /        \ /      (accepting: [1], [2])
      [0] --1--> [1] --0--> [2]
 >>
+  The automata for [rldicr] is
+<<
+      0          1
+     / \        / \
+     \ /        \ /          (accepting: [1])
+     [0] --1--> [1]
+>>
 *)
 
-Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_Sbad.
+Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_S2 | RLL_Sbad.
 
 Definition rll_transition (s: rll_state) (b: bool) : rll_state :=
   match s, b with
-  | RLL_S0, false => RLL_S0
   | RLL_S0, true => RLL_S1
+  | RLL_S1, false => RLL_S2
   | RLL_S1, true => RLL_S1
+  | RLL_S2, false => RLL_S2
   | _, _ => RLL_Sbad
   end.
 
 Definition rll_accepting (s: rll_state) : bool :=
   match s with
-  | RLL_S1 => true
+  | RLL_S1 | RLL_S2 => true
   | _ => false
   end.
 
-Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_S2 | RLR_Sbad.
+Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_Sbad.
 
 Definition rlr_transition (s: rlr_state) (b: bool) : rlr_state :=
   match s, b with
+  | RLR_S0, false => RLR_S0
   | RLR_S0, true => RLR_S1
-  | RLR_S1, false => RLR_S2
   | RLR_S1, true => RLR_S1
-  | RLR_S2, false => RLR_S2
   | _, _ => RLR_Sbad
   end.
 
 Definition rlr_accepting (s: rlr_state) : bool :=
   match s with
-  | RLR_S1 | RLR_S2 => true
+  | RLR_S1 => true
   | _ => false
   end.
 
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
 }.