new syntax for local and global directives

theories/additions/Dichotomy.v

@@ -128,7 +128,7 @@ Proof.
     discriminate.
 Qed.
 
-Global Hint Resolve dicho_aux_le_xOXO dicho_aux_le_xOXI 
+#[global] Hint Resolve dicho_aux_le_xOXO dicho_aux_le_xOXI 
              dicho_aux_le_xIXO dicho_aux_le_xIXI : chains.
 
 Lemma dicho_aux_lt : forall p, 3 < p ->

theories/additions/Euclidean_Chains.v

@@ -489,7 +489,7 @@ $2^k.3^p$, using Fcompose and previous lemmas.
 Let us look at a simple example *)
 
 (* begin snippet F144 *)
-Global Hint Resolve F1_correct F1_proper
+#[global] Hint Resolve F1_correct F1_proper
      F3_correct F3_proper Fcompose_correct Fcompose_proper
      Fexp2_correct Fexp2_proper : chains.
 
@@ -858,7 +858,7 @@ Lemma KFK_proper : Kchain_proper (KFK kbr fq).
          * rewrite H2, H3;reflexivity. 
 Qed.
 
-Global Instance KFF_proper : Fchain_proper (KFF kbr fq).
+#[global] Instance KFF_proper : Fchain_proper (KFF kbr fq).
  Proof.
    intros until M; intros k k' Hk Hk' H x y Hxy;
    unfold KFF;   simpl.
@@ -1042,7 +1042,7 @@ Proof.
 Qed.
 
 (* begin snippet HintKchains *)
-Global Hint Resolve KFF_correct KFF_proper KFK_correct KFK_proper : chains.
+#[global] Hint Resolve KFF_correct KFF_proper KFK_correct KFK_proper : chains.
 (* end snippet HintKchains *)
 
 Lemma k3_1_correct : Kchain_correct 3 1 k3_1.
@@ -1059,7 +1059,7 @@ Proof.
   add_op_proper M H3; rewrite H2; reflexivity.
 Qed.
 
-Global Hint Resolve k3_1_correct k3_1_proper : chains.
+#[global] Hint Resolve k3_1_correct k3_1_proper : chains.
 
 (** an example of correct chain construction  *)
 
@@ -1185,7 +1185,7 @@ Definition  OK (s: signature)
 
 (* end snippet dependentlyTypedFuns *)
 
-Global Hint Resolve pos_gt_3 : chains.
+#[global] Hint Resolve pos_gt_3 : chains.
 
 (* begin snippet GammaContext *)
 Section Gamma.

theories/additions/FirstSteps.v

@@ -14,8 +14,8 @@ Section Definitions.
            (mult : A -> A -> A)
            (one : A).
 
-Local Infix "*" := mult.
-Local Notation "1" := one.
+#[local] Infix "*" := mult.
+#[local] Notation "1" := one.
 
 (**  Naive (linear) implementation *)
 

theories/additions/Monoid_def.v

@@ -178,9 +178,9 @@ Every instance of class  [Monoid] can be transformed into an instance of
 *)
 
 (* begin snippet Coerciona:: no-out  *)
-Global Instance eq_equiv {A} : Equiv A := eq.
+#[global] Instance eq_equiv {A} : Equiv A := eq.
 
-Global Instance Monoid_EMonoid `(M:@Monoid A op one) :
+#[global] Instance Monoid_EMonoid `(M:@Monoid A op one) :
         EMonoid  op one eq_equiv.
 Proof.
 split; unfold eq_equiv, equiv in *.

theories/additions/Monoid_instances.v

@@ -194,9 +194,9 @@ Qed.
 
 (* begin snippet M2Defsb:: no-out *)
 
-Global Instance M2_op : Mult_op M2 := M2_mult.
+#[global] Instance M2_op : Mult_op M2 := M2_mult.
 
-Global Instance M2_Monoid : Monoid   M2_op Id2.
+#[global] Instance M2_Monoid : Monoid   M2_op Id2.
 (* ... *)
 (* end snippet M2Defsb *)
 Proof. 
@@ -236,7 +236,7 @@ Section Nmodulo.
     intro H;subst m. discriminate. 
   Qed.
 
-  Local Hint Resolve m_neq_0 : chains.
+  #[local] Hint Resolve m_neq_0 : chains.
 
   (* begin snippet Nmodulob:: no-out *)
   Definition mult_mod (x y : N) := (x * y) mod m.
@@ -256,7 +256,7 @@ Section Nmodulo.
   Qed.
 
   (* begin snippet Nmoduloc:: no-out *)
-  Global Instance mult_mod_proper :
+  #[global] Instance mult_mod_proper :
     Proper (mod_equiv ==> mod_equiv ==> mod_equiv) mod_op.
   (* end snippet Nmoduloc *)
   Proof.
@@ -269,7 +269,7 @@ Section Nmodulo.
   Qed.
 
   (* begin snippet Nmodulod:: no-out *)
-  Local  Open Scope M_scope.
+  #[local]  Open Scope M_scope.
 
   Lemma mult_mod_associative :  forall x y z,
       x * (y * z) = x * y * z.
@@ -299,7 +299,7 @@ Section Nmodulo.
 
 
   (* begin snippet Nmodulog:: no-out *)  
-  Global Instance Nmod_Monoid : EMonoid  mod_op 1 mod_equiv.
+  #[global] Instance Nmod_Monoid : EMonoid  mod_op 1 mod_equiv.
   (* end snippet Nmodulog *)
   Proof.
     unfold equiv, mod_equiv, mod_eq, mult_op, mod_op, mult_mod.
@@ -318,7 +318,7 @@ Section S256.
 
   Let mod256 :=  mod_op 256.
 
-  Local Existing Instance mod256 | 1.
+  #[local] Existing Instance mod256 | 1.
 
   Compute (211 * 67)%M.
 

theories/additions/More_on_positive.v

@@ -23,7 +23,7 @@ Proof.
   discriminate.
 Qed.
 
-Global Hint Resolve Pos_to_nat_neq_0 : chains.
+#[global] Hint Resolve Pos_to_nat_neq_0 : chains.
 
 
 (** ** Relationship with [nat] and [N] 
@@ -34,7 +34,7 @@ Proof. discriminate. Qed.
 Lemma Npos_gt_0 : forall p, (0 < N.pos p)%N.
 Proof. reflexivity. Qed.
 
-Global Hint Resolve Npos_diff_zero  Npos_gt_0 : chains.
+#[global] Hint Resolve Npos_diff_zero  Npos_gt_0 : chains.
 
 
 Lemma pos2N_inj_lt : forall n p, (n < p)%positive <-> (N.pos n < N.pos p)%N.
@@ -87,7 +87,7 @@ Proof.
  apply Pos2Nat.inj_le; apply pos_le_mul.
 Qed.
 
-Global Hint Resolve Pos2Nat_le_1_p : chains.
+#[global] Hint Resolve Pos2Nat_le_1_p : chains.
 
 (** ** Surjection from [N] into [positive] 
 *)
@@ -239,7 +239,7 @@ Proof.
  -  split; intros; now compute.
 Qed.
 
-Global Hint Resolve pos_gt_3 : chains.
+#[global] Hint Resolve pos_gt_3 : chains.
 
 (** ** Lemmas on Euclidean division 
     N.pos_div_eucl (a:positive) (b:N) : N * N 

theories/additions/Naive.v

@@ -64,7 +64,7 @@ is still of type [nat].
 *)
 
 Module N_mod.
-Local Open Scope N_scope.
+#[local] Open Scope N_scope.
 
 Section m_fixed.
 

theories/additions/Pow.v

@@ -140,7 +140,7 @@ Section M_given.
           (M:EMonoid  E_op E_one E_eq).
 (* end snippet MGiven *)
 
-Global Instance Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op.
+#[global] Instance Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op.
 Proof.
   apply  Eop_proper.
 Qed.
@@ -157,7 +157,7 @@ Ltac monoid_simpl := repeat monoid_rw.
 (* *** Properties of the classical exponentiation  *)
 
 (* begin snippet powerProper:: no-out *)
-Global Instance power_proper :
+#[global] Instance power_proper :
   Proper (equiv ==> eq ==> equiv) power.
 (* end snippet powerProper *)
 Proof.
@@ -284,7 +284,7 @@ Proof.
     now monoid_rw.
 Qed.
 
-Global Instance Pos_bpow_proper :
+#[global] Instance Pos_bpow_proper :
   Proper  (equiv ==> eq ==> equiv) Pos_bpow.
 Proof.
   intros x y Hxy n p Hnp. subst n. revert  x y Hxy.

theories/additions/Pow_variant.v

@@ -127,7 +127,7 @@ Section M_given.
  Context (M:EMonoid  E_op E_one E_eq).
 
 
-Global Instance Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op.
+#[global] Instance Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op.
 apply  Eop_proper.
 Qed.
 
@@ -143,7 +143,7 @@ Ltac monoid_simpl := repeat monoid_rw.
 
 Section About_power.
 
-Global Instance power_proper : Proper (equiv ==> eq ==> equiv) power.
+#[global] Instance power_proper : Proper (equiv ==> eq ==> equiv) power.
 Proof.
   intros x y Hxy n p Hnp;  subst p; induction n.
   - reflexivity.

theories/ordinals/Ackermann/misc.v

@@ -1,6 +1,6 @@
 Require Import Eqdep_dec.
 
-Global Set Asymmetric Patterns.
+#[global] Set Asymmetric Patterns.
 
 Lemma inj_right_pair2 :
  forall A : Set,

theories/ordinals/Epsilon0/Canon.v

@@ -1104,7 +1104,8 @@ Proof.
   simpl;   apply T1limit_canonS_not_zero; auto.
 Qed.
 
-Global Hint Resolve CanonS_lt Canon_lt Canon_of_limit_not_null : E0.
+#[global]
+  Hint Resolve CanonS_lt Canon_lt Canon_of_limit_not_null : E0.
 
 Lemma CanonS_phi0_Succ alpha i : CanonS (E0phi0 (E0succ alpha)) i =
                                  Omega_term alpha i.

theories/ordinals/Epsilon0/E0.v

@@ -345,7 +345,7 @@ Proof.
 Defined.
 (* end snippet E0LtWf *)
 
-Global Hint Resolve E0lt_wf : E0.
+#[global] Hint Resolve E0lt_wf : E0.
 
 Lemma Lt_Succ_Le (alpha beta: E0):  beta o< alpha -> E0succ beta o<= alpha.
 Proof.
@@ -397,14 +397,14 @@ Proof.
     apply LT_succ;auto.
 Qed.
 
-Global Hint Resolve E0pred_Lt : E0.
+#[global] Hint Resolve E0pred_Lt : E0.
 
 
 Lemma Succ_Succb (alpha : E0) : E0is_succ (E0succ alpha).
 destruct alpha; unfold E0is_succ, E0succ; cbn; apply T1.succ_is_succ.
 Qed.
 
-Global Hint Resolve Succ_Succb : E0.
+#[global] Hint Resolve Succ_Succb : E0.
 
 Ltac ord_eq alpha beta := assert (alpha = beta);
       [apply E0_eq_intro ; try reflexivity|].
@@ -451,7 +451,8 @@ Proof.
   intros H H0. rewrite (succ_not_limit _ H) in H0. discriminate.  
 Qed.
 
-Global Hint Resolve Limit_not_Zero Succ_not_Zero Lt_Succ Succ_not_T1limit : E0.
+#[global]
+  Hint Resolve Limit_not_Zero Succ_not_Zero Lt_Succ Succ_not_T1limit : E0.
 
 Lemma lt_Succ_inv : forall alpha beta, beta o< alpha <->
                                        E0succ beta o<= alpha.

theories/ordinals/Epsilon0/Epsilon0rpo.v

@@ -173,7 +173,7 @@ Proof.
  simpl; auto with arith.
 Qed.
 
-Global Hint Resolve T1_size2 T1_size3 : rpo.
+#[global] Hint Resolve T1_size2 T1_size3 : rpo.
 
 
 (** let us recall subterm properties on T1 *)
@@ -198,9 +198,9 @@ Proof.
 Qed.
 
 
-Global Hint Resolve nat_lt_cons : rpo.
-Global Hint Resolve lt_subterm2 lt_subterm1 : rpo.
-Global Hint Resolve T1_size3 T1_size2 T1_size1 : rpo.
+#[global] Hint Resolve nat_lt_cons : rpo.
+#[global] Hint Resolve lt_subterm2 lt_subterm1 : rpo.
+#[global] Hint Resolve T1_size3 T1_size2 T1_size1 : rpo.
 
 
 Lemma nat_2_term_mono : forall n n', (n < n')%nat -> 
@@ -404,29 +404,29 @@ Remark R1 : Acc P.prec nat_0.
   destruct y; try contradiction.
 Qed.
 
-Global Hint Resolve R1 : rpo.
+#[global] Hint Resolve R1 : rpo.
 
 Remark R2 : Acc P.prec ord_zero. 
   split.
   destruct y; try contradiction; auto with rpo.
 Qed.
 
-Global Hint Resolve R2 : rpo.
+#[global] Hint Resolve R2 : rpo.
 
 Remark R3 : Acc P.prec nat_S.
   split.
   destruct y; try contradiction;auto with rpo.
 Qed.
 
 
-Global Hint Resolve R3 : rpo.
+#[global] Hint Resolve R3 : rpo.
 
 Remark R4 : Acc P.prec ord_cons.
   split.
   destruct y; try contradiction;auto with rpo.
 Qed.
 
-Global Hint Resolve R4 : rpo.
+#[global] Hint Resolve R4 : rpo.
 
 Theorem well_founded_rpo : well_founded rpo.
 Proof.
@@ -439,7 +439,7 @@ Section  well_founded.
 
   Let R := restrict  nf lt.
 
-  Local Hint Unfold restrict R : rpo.
+  #[local] Hint Unfold restrict R : rpo.
 
   Lemma R_inc_rpo : forall o o', R o o' -> rpo (T1_2_term o) (T1_2_term o').
   Proof.

theories/ordinals/Epsilon0/F_alpha.v

@@ -278,15 +278,15 @@ Section Properties.
       rewrite F_zero_eqn. rewrite LF1; abstract lia.
     Qed.
 
-    Local Hint Resolve F_One_Zero_dom mono_F_Zero Lt_n_F_Zero_n : T1.
+    #[local] Hint Resolve F_One_Zero_dom mono_F_Zero Lt_n_F_Zero_n : T1.
 
     Lemma F_One_Zero_ge :  F_ E0zero <<= F_ 1.
     Proof.
       intro n; destruct n;
         rewrite F_zero_eqn, LF1; abstract lia.  
     Qed. 
 
-    Local Hint Resolve  F_One_Zero_ge : T1.
+    #[local] Hint Resolve  F_One_Zero_ge : T1.
 
     Lemma PZero : P E0zero.
     Proof. 

theories/ordinals/Epsilon0/Hprime.v

@@ -599,7 +599,7 @@ Section Proof_of_Abstract_Properties.
       - apply Succ_Succb.
     Qed.
 
-    Local Hint Resolve PD_Zero PA_Zero : E0.
+    #[local] Hint Resolve PD_Zero PA_Zero : E0.
 
     Lemma PC_Zero :  H'_ E0zero <<= H'_ (E0succ E0zero).
     Proof.
@@ -608,7 +608,7 @@ Section Proof_of_Abstract_Properties.
       rewrite E0pred_of_Succ, H'_eq1; auto with arith.
     Qed. 
 
-    Local Hint Resolve  PC_Zero : core.
+    #[local] Hint Resolve  PC_Zero : core.
 
     Lemma PZero : P E0zero.
     Proof. 

theories/ordinals/Epsilon0/L_alpha.v

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

theories/ordinals/Epsilon0/Large_Sets_Examples.v

@@ -56,7 +56,7 @@ Compute  (gnaw (T1omega * T1omega) (interval 6 699)).
 
 Compute pp (  gnaw (T1omega * T1omega) (interval 6 509)).
 
-Global Hint Resolve iota_from_lt_not_In: core.
+#[global] Hint Resolve iota_from_lt_not_In: core.
 
 (* begin snippet Ex1Lemma:: no-out *)
 Example Ex1 : mlarge (T1omega * T1omega) (interval 6 510).