diff --git a/theories/countable.v b/theories/countable.v
index 0d32ba0db9eb9fa8ff8c6b874257873d4a65a385..4894b0b12c15bfbda481b2facd513c16ce9021dc 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -269,7 +269,7 @@ Next Obligation.
 Qed.
 
 (** ** Generic trees *)
-Close Scope positive.
+Local Close Scope positive.
 
 Inductive gen_tree (T : Type) : Type :=
   | GenLeaf : T → gen_tree T
diff --git a/theories/numbers.v b/theories/numbers.v
index f039f968c23185d3143d8118d6fcd0adda4c1f33..7ecce34d2558d5d10839a95079e11fe2eb1e4c71 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -7,7 +7,7 @@ From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
 From Coq Require Import QArith Qcanon.
 From stdpp Require Export base decidable option.
 Set Default Proof Using "Type".
-Open Scope nat_scope.
+Local Open Scope nat_scope.
 
 Coercion Z.of_nat : nat >-> Z.
 Instance comparison_eq_dec : EqDecision comparison.
@@ -124,7 +124,7 @@ Definition max_list_with {A} (f : A → nat) : list A → nat :=
 Notation max_list := (max_list_with id).
 
 (** * Notations and properties of [positive] *)
-Open Scope positive_scope.
+Local Open Scope positive_scope.
 
 Typeclasses Opaque Pos.le.
 Typeclasses Opaque Pos.lt.
@@ -289,7 +289,7 @@ Proof.
   - reflexivity.
 Qed.
 
-Close Scope positive_scope.
+Local Close Scope positive_scope.
 
 (** * Notations and properties of [N] *)
 Typeclasses Opaque N.le.
@@ -334,7 +334,7 @@ Proof. repeat intro; lia. Qed.
 Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
 
 (** * Notations and properties of [Z] *)
-Open Scope Z_scope.
+Local Open Scope Z_scope.
 
 Typeclasses Opaque Z.le.
 Typeclasses Opaque Z.lt.
@@ -474,7 +474,7 @@ Lemma Z_succ_pred_induction y (P : Z → Prop) :
   (∀ x, P x).
 Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
 
-Close Scope Z_scope.
+Local Close Scope Z_scope.
 
 (** * Injectivity of casts *)
 Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
@@ -488,7 +488,7 @@ Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
 Typeclasses Opaque Qcle.
 Typeclasses Opaque Qclt.
 
-Open Scope Qc_scope.
+Local Open Scope Qc_scope.
 Delimit Scope Qc_scope with Qc.
 Notation "1" := (Q2Qc 1) : Qc_scope.
 Notation "2" := (1+1) : Qc_scope.
@@ -648,7 +648,7 @@ Proof.
   apply Qc_is_canon; simpl.
   by rewrite !Qred_correct, <-inject_Z_opp, <-inject_Z_plus.
 Qed.
-Close Scope Qc_scope.
+Local Close Scope Qc_scope.
 
 (** * Positive rationals *)
 (** The theory of positive rationals is very incomplete. We merely provide
diff --git a/theories/strings.v b/theories/strings.v
index 7f3d29ba339f82d8e699fc91eb60155da46a1f58..c96ea2be9be68cd954540f9938bda24c6fe37ffe 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -12,6 +12,8 @@ Notation length := List.length.
 
 (** * Fix scopes *)
 Open Scope string_scope.
+(* Make sure [list_scope] has priority over [string_scope], so that
+   the "++" notation designates list concatenation. *)
 Open Scope list_scope.
 Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
 Arguments String.append : simpl never.