diff --git a/theories/dfa.v b/theories/dfa.v
index 3f6b9d8..73982cc 100644
--- a/theories/dfa.v
+++ b/theories/dfa.v
@@ -11,7 +11,7 @@ Unset Strict Implicit.
 
 Section FA.
 Variable char : finType.
-Local Notation word := (word char).
+#[local] Notation word := (word char).
 
 (** * Deterministic Finite Automata *)
 
@@ -157,7 +157,7 @@ Qed.
 Section CutOff.
   Variables (aT rT : finType) (f : seq aT -> rT).
   Hypothesis RC_f : forall x y a, f x = f y -> f (x++[::a]) = f (y++[::a]).
-  Local Set Default Proof Using "RC_f".
+  #[local] Set Default Proof Using "RC_f".
 
   Lemma RC_seq x y z : f x = f y -> f (x++z) = f (y++z).
   Proof.
@@ -436,7 +436,7 @@ Section NonRegular.
   Qed.
 
   Hypothesis (a b : char) (Hab : a != b).
-  Local Set Default Proof Using "Hab".
+  #[local] Set Default Proof Using "Hab".
 
   Definition Lab w := exists n, w = nseq n a ++ nseq n b.
 
diff --git a/theories/languages.v b/theories/languages.v
index 8aea569..48449af 100644
--- a/theories/languages.v
+++ b/theories/languages.v
@@ -49,7 +49,7 @@ Section HomDef.
 
   Definition homomorphism := forall w1 w2, h (w1 ++ w2) = h w1 ++ h w2.
   Hypothesis h_hom : homomorphism.
-  Local Set Default Proof Using "h_hom".
+  #[local] Set Default Proof Using "h_hom".
 
   Lemma h0 : h [::] = [::].
   Proof.
diff --git a/theories/minimization.v b/theories/minimization.v
index e8b2bdc..435fced 100644
--- a/theories/minimization.v
+++ b/theories/minimization.v
@@ -11,14 +11,14 @@ Set Implicit Arguments.
 Unset Printing Implicit Defensive.
 Unset Strict Implicit.
 
-Local Open Scope quotient_scope.
+#[local] Open Scope quotient_scope.
 
 (** * DFA Minimization *)
 
 Section Minimization.
 Variable (char : finType).
-Local Notation word := (word char).
-Local Notation dfa := (dfa char).
+#[local] Notation word := (word char).
+#[local] Notation dfa := (dfa char).
 
 Definition coll (A : dfa) x y := forall w, (delta x w \in dfa_fin A) = (delta y w \in dfa_fin A).
 
diff --git a/theories/misc.v b/theories/misc.v
index 03a1c1b..40fa458 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -121,7 +121,7 @@ Proof. rewrite -!cardsT -powersetT. exact: card_powerset. Qed.
 
 (** Miscellaneous *)
 
-Local Open Scope quotient_scope.
+#[local] Open Scope quotient_scope.
 Lemma epiK {T:choiceType} (e : equiv_rel T) x : e (repr (\pi_{eq_quot e} x)) x.
 Proof. by rewrite -eqmodE reprK. Qed.
 
diff --git a/theories/myhill_nerode.v b/theories/myhill_nerode.v
index d3388ce..11679a6 100644
--- a/theories/myhill_nerode.v
+++ b/theories/myhill_nerode.v
@@ -20,7 +20,7 @@ exist most general classifiers corresponding to minimal automata. *)
 Section Clasifiers.
 
 Variable char: finType.
-Local Notation word := (word char).
+#[local] Notation word := (word char).
 
 Record classifier := Classifier {
   classifier_classes : finType;
diff --git a/theories/nfa.v b/theories/nfa.v
index fff2529..1a813fd 100644
--- a/theories/nfa.v
+++ b/theories/nfa.v
@@ -11,7 +11,7 @@ Unset Strict Implicit.
 
 Section NFA.
 Variable char : finType.
-Local Notation word := (word char).
+#[local] Notation word := (word char).
 
 (** * Nondeterministic Finite Automata.