Fix Coq 8.14 instance locality deprecation warnings.

_CoqProject

@@ -5,8 +5,9 @@
 
 -arg -w -arg -notation-overridden
 -arg -w -arg -ambiguous-paths
--arg -w -arg -deprecated-instance-without-locality
 -arg -w -arg -deprecated-hint-rewrite-without-locality
+-arg -w -arg -unknown-option
+-arg -w -arg -deprecated-option
 
 theories/ordinals/OrdinalNotations/ON_Omega.v
 theories/ordinals/OrdinalNotations/ON_Generic.v

theories/additions/AM.v

@@ -195,15 +195,15 @@ end.
 
 
 
-Instance Stack_equiv_refl {A}`{M : @EMonoid A op one equ} :
+#[ global ] Instance Stack_equiv_refl {A}`{M : @EMonoid A op one equ} :
   Reflexive stack_equiv.
 Proof.
   red; intros. induction x.
   - now left.
   - right; [reflexivity | assumption].
 Qed.
 
-Instance Stack_equiv_equiv {A}`{M : @EMonoid A op one equ}:
+#[ global ] Instance Stack_equiv_equiv {A}`{M : @EMonoid A op one equ}:
   Equivalence stack_equiv.
 Proof.
  split.
@@ -227,7 +227,7 @@ Proof.
            eapply IHx;eauto.
 Qed.
 
-Instance result_equiv_equiv `{M : @EMonoid A op one equ}:
+#[ global ] Instance result_equiv_equiv `{M : @EMonoid A op one equ}:
   Equivalence result_equiv.
 Proof.
   split.
@@ -298,7 +298,7 @@ Proof.
 Qed.
 
 
-Instance exec_Proper `{M : @EMonoid A op one equ} :
+#[ global ] Instance exec_Proper `{M : @EMonoid A op one equ} :
   Proper (Logic.eq ==> equiv ==> stack_equiv ==> result_equiv) (@exec A op) .
 Proof.
  intros c c' Hx x x' Hequiv s s' Hs; subst.

theories/additions/BinaryStrat.v

@@ -19,12 +19,12 @@ Definition half (p:positive) :=
 
 Definition two (p:positive) := 2%positive.
 
-Instance Binary_strat : Strategy half.
+#[ global ] Instance Binary_strat : Strategy half.
 Proof.
   split; destruct p; unfold half; try lia.
 Qed.
 
-Instance Two_strat : Strategy two.
+#[ global ] Instance Two_strat : Strategy two.
 Proof.
   split;unfold two; lia.
 Qed.

theories/additions/Dichotomy.v

@@ -186,7 +186,7 @@ Qed.
 
 
 (* begin snippet DichoStrat:: no-out *)
-Instance Dicho_strat : Strategy dicho.
+#[ global ] Instance Dicho_strat : Strategy dicho.
 (* end snippet DichoStrat *)
 Proof.
   split.

theories/additions/Euclidean_Chains.v

@@ -192,11 +192,11 @@ Definition computation_equiv {A:Type} (op: Mult_op A)
    computation_execute op c == computation_execute op c'.
 
 
-Instance Comp_equiv {A:Type} (op: Mult_op A) (equiv : Equiv A):
+#[ global ] Instance Comp_equiv {A:Type} (op: Mult_op A) (equiv : Equiv A):
   Equiv (@computation A) :=
   @computation_equiv A op equiv.
 
-Instance comp_equiv_equivalence {A:Type} (op: Mult_op A)
+#[ global ] Instance comp_equiv_equivalence {A:Type} (op: Mult_op A)
            (equiv : Equiv A) : Equivalence  equiv ->
                                Equivalence (computation_equiv op equiv).   
 Proof.
@@ -219,7 +219,7 @@ Class Fkont_proper
 
 
 
-Instance Return_proper `(M : @EMonoid A op E_one E_equiv) :
+#[ global ] Instance Return_proper `(M : @EMonoid A op E_one E_equiv) :
   Fkont_proper M (@Return A).
 Proof.
  intros x y Hxy; assumption.
@@ -326,7 +326,7 @@ Class Fchain_proper (fc : Fchain) := Fchain_proper_bad_prf :
 (* end snippet Bad3 *)
 
 (* begin snippet Bad3b:: no-out *)
-Instance Fcompose_proper (f1 f2 : Fchain)
+#[ global ] Instance Fcompose_proper (f1 f2 : Fchain)
          (_ : Fchain_proper f1)
          (_ : Fchain_proper f2) :
   Fchain_proper (Fcompose f1 f2).
@@ -361,15 +361,15 @@ Class Fchain_proper (fc : Fchain) := Fchain_proper_prf :
 (* end snippet correctProper *)
 
 (* begin snippet F1proper:: no-out *)
-Instance F1_proper : Fchain_proper F1.
+#[ global ] Instance F1_proper : Fchain_proper F1.
 Proof.
   intros until M ; intros k k' Hk Hk' H a b H0; unfold F1; cbn;
   now apply H.  
 Qed.
 (* end snippet F1proper *)
 
 (* begin snippet F3proper:: no-out *)
-Instance F3_proper : Fchain_proper F3.
+#[ global ] Instance F3_proper : Fchain_proper F3.
 (* end snippet F3proper *)
 Proof.
   intros  A op one equiv M  k k' Hk Hk'  Hkk' x y Hxy;  
@@ -378,7 +378,7 @@ Proof.
 Qed.
 
 (* begin snippet F2proper:: no-out *)
-Instance F2_proper : Fchain_proper F2.
+#[ global ] Instance F2_proper : Fchain_proper F2.
 (* end snippet F2proper *)
 Proof.
   intros  A op one equiv M  k k' Hk Hk'  Hkk' x y Hxy;  
@@ -423,7 +423,7 @@ Proof.
 Qed.
 
 (* begin snippet FcomposeProper:: no-out *)
-Instance Fcompose_proper (fc1 fc2: Fchain)
+#[ global ] Instance Fcompose_proper (fc1 fc2: Fchain)
                          (_ : Fchain_proper fc1)
                          (_ : Fchain_proper fc2) :
   Fchain_proper (Fcompose fc1 fc2).
@@ -436,7 +436,7 @@ Proof.
 Qed.
 
 
-Instance Fexp2_nat_proper (n:nat) : 
+#[ global ] Instance Fexp2_nat_proper (n:nat) : 
                            Fchain_proper (Fexp2_of_nat n).
 Proof.
   induction n; cbn.
@@ -473,7 +473,7 @@ Proof.
 Qed.
 
 (* begin snippet Fexp2Proper:: no-out *)
-Instance  Fexp2_proper (p:positive) : Fchain_proper (Fexp2 p).
+#[ global ] Instance  Fexp2_proper (p:positive) : Fchain_proper (Fexp2 p).
 (* end snippet Fexp2Proper *)
 Proof.
   unfold  Fexp2; apply Fexp2_nat_proper.
@@ -631,7 +631,7 @@ Kchain_proper_prf :
 (* end snippet KchainCorrectDef *)
 
 (* begin snippet K73Ok:: no-out *)
-Instance k7_3_proper : Kchain_proper k7_3.
+#[ global ] Instance k7_3_proper : Kchain_proper k7_3.
 Proof.
   intros until M; intros; red; unfold k7_3; cbn;
   add_op_proper M H3; apply H1;  rewrite H2;   reflexivity. 
@@ -690,7 +690,7 @@ Proof.
 Qed.
 
 (* begin snippet K2FProper:: no-out *)
-Instance K2F_proper (kc : Kchain)(_ : Kchain_proper kc) :
+#[ global ] Instance K2F_proper (kc : Kchain)(_ : Kchain_proper kc) :
   Fchain_proper (K2F kc).
 (* end snippet K2FProper *)
 Proof.
@@ -981,7 +981,7 @@ Proof.
 Qed.
 
 (* begin snippet FFKProper:: no-out *)
-Instance FFK_proper 
+#[ global ] Instance FFK_proper 
          (fp fq : Fchain)
          (_ :   Fchain_proper fp)
          (_ :  Fchain_proper fq)
@@ -1030,7 +1030,7 @@ Proof.
     + generalize (power_eq3 a);simpl;now symmetry.
 Qed.
 
-Instance  FK_proper  (Fp : Fchain) (_ : Fchain_proper Fp):
+#[ global ] Instance  FK_proper  (Fp : Fchain) (_ : Fchain_proper Fp):
   Kchain_proper (FK Fp).
 Proof.
   unfold FK; intros until M; intros k k' x y  H0 H1 H2 H3. 

theories/additions/Fib2.v

@@ -53,7 +53,7 @@ Lemma neutral_r p : mul2 p (0,1)  = p.
 Qed.
 
 (* begin snippet mul2Monoid  *)
-Instance Mul2 : Monoid  mul2 (0,1).
+#[ global ] Instance Mul2 : Monoid  mul2 (0,1).
 (* end snippet mul2Monoid  *)
 
 Proof.

theories/additions/Monoid_def.v

@@ -52,7 +52,7 @@ End Demo.
 
 (* begin snippet DemoStringMult:: no-out *)
 
-Instance string_op : Mult_op string := append.
+#[ global ] Instance string_op : Mult_op string := append.
 Open Scope string_scope.
 
 Example ex_string : "ab" * "cde" = "abcde".
@@ -61,7 +61,7 @@ Proof. reflexivity. Qed.
 (* end snippet DemoStringMult *)
 
 
-Instance bool_and_binop : Mult_op bool := andb.
+#[ global ] Instance bool_and_binop : Mult_op bool := andb.
 
 Example ex_bool : true * false = false.
 Proof. reflexivity. Qed.
@@ -141,25 +141,25 @@ Class EMonoid (A:Type)(E_op : Mult_op A)(E_one : A)
 (* end snippet EMonoidDef *)
 
 
-Instance Equiv_Equiv (A:Type)(E_op : Mult_op A)(E_one : A) 
+#[ global ] Instance Equiv_Equiv (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
    Equivalence E_eq.
 destruct M;auto.
 Qed.
 
-Instance Equiv_Refl (A:Type)(E_op : Mult_op A)(E_one : A) 
+#[ global ] Instance Equiv_Refl (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
    Reflexive E_eq.
 destruct (Equiv_Equiv   M);auto.
 Qed.
 
-Instance Equiv_Sym (A:Type)(E_op : Mult_op A)(E_one : A) 
+#[ global ] Instance Equiv_Sym (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
    Symmetric E_eq.
 destruct (Equiv_Equiv   M);auto.
 Qed.
 
-Instance Equiv_Trans (A:Type)(E_op : Mult_op A)(E_one : A) 
+#[ global ] Instance Equiv_Trans (A:Type)(E_op : Mult_op A)(E_one : A) 
       (E_eq: Equiv A)(M :EMonoid E_op E_one E_eq) :
    Transitive E_eq.
 destruct (Equiv_Equiv   M);auto.

theories/additions/Monoid_instances.v

@@ -17,17 +17,17 @@ Open Scope Z_scope.
 (** *** Multiplicative monoid on [Z] *)
 
 (* begin snippet ZMultDef *)
-Instance Z_mult_op : Mult_op Z := Z.mul.
+#[ global ] Instance Z_mult_op : Mult_op Z := Z.mul.
 
-Instance ZMult : Monoid  Z_mult_op 1. (* .no-out *)
+#[ global ] Instance ZMult : Monoid  Z_mult_op 1. (* .no-out *)
 Proof. (* .no-out *)
   split.
     all: unfold Z_mult_op, mult_op;intros;ring.
 Qed.
 (* end snippet ZMultDef *)
 
 
-Instance ZMult_Abelian : Abelian_Monoid ZMult.
+#[ global ] Instance ZMult_Abelian : Abelian_Monoid ZMult.
 Proof.
   split; exact Zmult_comm.
 Qed.
@@ -37,9 +37,9 @@ Qed.
 
 (* begin snippet natMult:: no-out *)
 
-Instance nat_mult_op : Mult_op nat | 5 := Nat.mul.
+#[ global ] Instance nat_mult_op : Mult_op nat | 5 := Nat.mul.
 
-Instance  Natmult : Monoid nat_mult_op  1%nat | 5.
+#[ global ] Instance  Natmult : Monoid nat_mult_op  1%nat | 5.
 Proof.
    split;unfold nat_mult_op, mult_op; intros; ring.
 Qed.
@@ -53,9 +53,9 @@ equal to $n$. See Sect.%~\ref{chains-exponent}.
 *)
 
 (* begin snippet natPlus:: no-out *)
-Instance nat_plus_op : Mult_op nat | 12 := Nat.add.
+#[ global ] Instance nat_plus_op : Mult_op nat | 12 := Nat.add.
 
-Instance Natplus : Monoid nat_plus_op  0%nat | 12.
+#[ global ] Instance Natplus : Monoid nat_plus_op  0%nat | 12.
 Proof.
    split;unfold nat_plus_op, mult_op; intros; ring.
 Qed.
@@ -65,9 +65,9 @@ Qed.
 
 Open Scope N_scope.
 
-Instance N_mult_op  : Mult_op N | 5 := N.mul.
+#[ global ] Instance N_mult_op  : Mult_op N | 5 := N.mul.
 
-Instance NMult : Monoid N_mult_op 1 | 5.
+#[ global ] Instance NMult : Monoid N_mult_op 1 | 5.
 Proof.
   split;unfold N_mult_op, mult_op; intros; ring.
 Qed.
@@ -78,9 +78,9 @@ Check NMult : EMonoid  N.mul 1%N eq.
 (* end snippet CheckCoercion *)
 
 
-Instance N_plus_op  : Mult_op N | 12 := N.add.
+#[ global ] Instance N_plus_op  : Mult_op N | 12 := N.add.
 
-Instance NPlus : Monoid N_plus_op 0 | 12.
+#[ global ] Instance NPlus : Monoid N_plus_op 0 | 12.
 Proof.
   split;unfold N_plus_op, mult_op; intros; ring.
 Qed.
@@ -89,9 +89,9 @@ Qed.
 (** Multiplicative Monoid on [positive] 
 *)
 
-Instance P_mult_op : Mult_op positive | 5  := Pos.mul .
+#[ global ] Instance P_mult_op : Mult_op positive | 5  := Pos.mul .
 
-Instance PMult : Monoid P_mult_op xH | 5.
+#[ global ] Instance PMult : Monoid P_mult_op xH | 5.
 Proof.
  split;unfold P_mult_op, Mult_op;intros.  
  -  now rewrite Pos.mul_assoc.
@@ -114,9 +114,9 @@ The type [int31] is defined in Standard Library in Module
 *)
 
 (* begin snippet int31:: no-out *)
-Instance int31_mult_op : Mult_op int31 := mul31.
+#[ global ] Instance int31_mult_op : Mult_op int31 := mul31.
 
-Instance  Int31mult : Monoid int31_mult_op  1.
+#[ global ] Instance  Int31mult : Monoid int31_mult_op  1.
 Proof.
    split;unfold int31_mult_op, mult_op; intros; ring.
 Qed.

theories/ordinals/Epsilon0/E0.v

@@ -127,7 +127,7 @@ Proof.
   refine (@mkord (FS i)%t1 _);apply T1.nf_FS.
 Defined.
 
-Instance Fin (i:nat) : E0.
+#[ global ] Instance Fin (i:nat) : E0.
 Proof.
   destruct i as [|i]; [exact Zero | exact (FinS i)].
 Defined.
@@ -316,7 +316,7 @@ Proof.
     apply LT_trans.
  Qed.
 
-Instance compare_E0 : Compare E0 :=
+#[ global ] Instance compare_E0 : Compare E0 :=
  fun (alpha beta:E0) => compare (cnf alpha) (cnf beta).
 
 Lemma compare_correct (alpha beta : E0) :

theories/ordinals/Epsilon0/F_alpha.v

@@ -27,7 +27,7 @@ The following definition is not accepted by the [equations] plug-in.
 
  *)
 
-Instance Olt : WellFounded Lt := E0.Lt_wf.
+#[ global ] Instance Olt : WellFounded Lt := E0.Lt_wf.
 
 (* begin snippet FailDemo *)
 
@@ -60,7 +60,7 @@ Lemma call_lt_wf : well_founded call_lt.
   -  unfold Peano.lt; apply Nat.lt_wf_0. 
 Qed.
 
-Instance WF : WellFounded call_lt := call_lt_wf.
+#[ global ] Instance WF : WellFounded call_lt := call_lt_wf.
 
 (*  F_star (alpha,i) is intended to be the i-th iterate of F_ alpha *)
 

theories/ordinals/Epsilon0/Hprime.v

@@ -28,7 +28,7 @@ From Equations Require Import Equations.
 (** ** A variant of the Hardy Wainer hierarchy *)
 
 
-Instance Olt : WellFounded Lt := Lt_wf.
+#[ global ] Instance Olt : WellFounded Lt := Lt_wf.
 
 (* begin snippet HprimeDef *)
 

theories/ordinals/Epsilon0/L_alpha.v

@@ -13,7 +13,7 @@ From Coq Require Import ArithRing Lia.
 From Equations Require Import Equations.
 Import RelationClasses Relations.
 
-Instance Olt : WellFounded Lt := Lt_wf.
+#[ global ] Instance Olt : WellFounded Lt := Lt_wf.
 Global Hint Resolve Olt : E0.
 
 (** Using Coq-Equations for building a function which satisfies