new syntax for local and global directives

Author: Casteran

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,