diff --git a/stdpp/pretty.v b/stdpp/pretty.v
index f5ea9a339c61a609c55a8806131ea2cebb2c46da..6efb0dd91c9a60fb2b2451fb849993e94da06e64 100644
--- a/stdpp/pretty.v
+++ b/stdpp/pretty.v
@@ -113,7 +113,7 @@ Proof. apply _. Qed.
 Global Instance pretty_Z : Pretty Z := λ x,
   match x with
   | Z0 => "0" | Zpos x => pretty x | Zneg x => "-" +:+ pretty x
-  end%string.
+  end.
 Global Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
 Proof.
   unfold pretty, pretty_Z.
diff --git a/stdpp/strings.v b/stdpp/strings.v
index 7f63c3201143065118d26f5eda1d2438e579e49a..15f2d15545d780220c459551c1829304a51d780a 100644
--- a/stdpp/strings.v
+++ b/stdpp/strings.v
@@ -1,74 +1,27 @@
 From Coq Require Import Ascii.
-From Coq Require Export String.
+From Coq Require String.
 From stdpp Require Export list.
 From stdpp Require Import countable.
 From stdpp Require Import options.
 
-(** To avoid randomly ending up with [String.length] because this module is
-imported hereditarily somewhere. *)
-Notation length := List.length.
+(** We define the ascii/string methods in corresponding modules, similar to what
+is done for numbers. These modules should generally not be imported, e.g., use
+[Ascii.is_nat] instead. *)
 
-(** Enable the string literal and append notation in [stdpp_scope], making it
-possible to write string literals as "foo" instead of "foo"%string.
+(** To avoid poluting the global namespace, we export only the [string] data
+type (with its constructors and eliminators) and notations. *)
+Export String (string(..)).
+Export (notations) String.
+
+(** Enable the string literal and append notation in [stdpp_scope], making
+it possible to write string literals as "foo" instead of "foo"%string.
 One could also enable the string literal notation via [Open Scope string_scope]
-but that overrides various notations (e.g, [++] on [list], [=?] on [nat]) with
-the version for strings. *)
-String Notation string string_of_list_byte list_byte_of_string : stdpp_scope.
-Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
-Global Arguments String.append : simpl never.
-
-(** * Decision of equality *)
-Global Instance ascii_eq_dec : EqDecision ascii := ascii_dec.
-Global Instance string_eq_dec : EqDecision string.
-Proof. solve_decision. Defined.
-Global Instance string_app_inj s1 : Inj (=) (=) (String.append s1).
-Proof. intros ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
-
-Global Instance string_inhabited : Inhabited string := populate "".
-
-(* Reverse *)
-Fixpoint string_rev_app (s1 s2 : string) : string :=
-  match s1 with
-  | "" => s2
-  | String a s1 => string_rev_app s1 (String a s2)
-  end.
-Definition string_rev (s : string) : string := string_rev_app s "".
-
-Definition is_nat (x : ascii) : option nat :=
-  match x with
-  | "0" => Some 0
-  | "1" => Some 1
-  | "2" => Some 2
-  | "3" => Some 3
-  | "4" => Some 4
-  | "5" => Some 5
-  | "6" => Some 6
-  | "7" => Some 7
-  | "8" => Some 8
-  | "9" => Some 9
-  | _ => None
-  end%char.
-
-(* Break a string up into lists of words, delimited by white space *)
-Definition is_space (x : Ascii.ascii) : bool :=
-  match x with
-  | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
-  end%char.
-
-Fixpoint words_go (cur : option string) (s : string) : list string :=
-  match s with
-  | "" => option_list (string_rev <$> cur)
-  | String a s =>
-     if is_space a then option_list (string_rev <$> cur) ++ words_go None s
-     else words_go (Some (from_option (String a) (String a "") cur)) s
-  end.
-Definition words : string → list string := words_go None.
+but that overrides various notations (e.g, [=?] on [nat]) with the version for
+strings. *)
+String Notation string
+  String.string_of_list_byte String.list_byte_of_string : stdpp_scope.
 
-Ltac words s :=
-  match type of s with
-  | list string => s
-  | string => eval vm_compute in (words s)
-  end.
+Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
 
 (** * Encoding and decoding *)
 (** The [Countable] instance of [string] is particularly useful to allow strings
@@ -77,7 +30,11 @@ to be used as keys in [gmap].
 The encoding of [string] to [positive] is taken from
 https://github.com/xavierleroy/canonical-binary-tries/blob/v2/lib/String2pos.v.
 It avoids creating auxiliary data structures such as [list bool], thereby
-improving efficiency. *)
+improving efficiency.
+
+We first provide some [Local] helper functions and then define the [Countable]
+instances for encoding/decoding in the modules [Ascii] and [String]. End-users
+should always use these instances. *)
 Local Definition bool_cons_pos (b : bool) (p : positive) : positive :=
   if b then p~1 else p~0.
 Local Definition ascii_cons_pos (c : ascii) (p : positive) : positive :=
@@ -128,13 +85,78 @@ Defined.
 Local Lemma pos_to_string_string_to_pos s : pos_to_string (string_to_pos s) = s.
 Proof. induction s as [|[[][][][][][][][]]]; by f_equal/=. Qed.
 
-Global Program Instance string_countable : Countable string := {|
-  encode := string_to_pos; decode p := Some (pos_to_string p)
-|}.
-Solve Obligations with
-  naive_solver eauto using pos_to_string_string_to_pos with f_equal.
-
-Global Instance ascii_countable : Countable ascii :=
-  inj_countable (λ a, String a EmptyString)
-                (λ s, match s with String a _ => Some a | _ => None end)
-                (λ a, eq_refl).
+Module Ascii.
+  Global Instance eq_dec : EqDecision ascii := ascii_dec.
+
+  Global Program Instance countable : Countable ascii := {|
+    encode a := string_to_pos (String a EmptyString);
+    decode p := match pos_to_string p return _ with String a _ => Some a | _ => None end
+  |}.
+  Next Obligation. by intros [[] [] [] [] [] [] [] []]. Qed.
+
+  Definition is_nat (x : ascii) : option nat :=
+    match x with
+    | "0" => Some 0
+    | "1" => Some 1
+    | "2" => Some 2
+    | "3" => Some 3
+    | "4" => Some 4
+    | "5" => Some 5
+    | "6" => Some 6
+    | "7" => Some 7
+    | "8" => Some 8
+    | "9" => Some 9
+    | _ => None
+    end%char.
+
+  Definition is_space (x : ascii) : bool :=
+    match x with
+    | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
+    end%char.
+End Ascii.
+
+Module String.
+  (** Use a name that is consistent with [list]. *)
+  Notation app := String.append.
+
+  (** And obtain a proper behavior for [simpl]. *)
+  Global Arguments app : simpl never.
+
+  Global Instance eq_dec : EqDecision string.
+  Proof. solve_decision. Defined.
+  Global Instance app_inj s1 : Inj (=) (=) (app s1).
+  Proof. intros ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
+
+  Global Instance inhabited : Inhabited string := populate "".
+
+  Global Program Instance countable : Countable string := {|
+    encode := string_to_pos;
+    decode p := Some (pos_to_string p)
+  |}.
+  Solve Obligations with
+    naive_solver eauto using pos_to_string_string_to_pos with f_equal.
+
+  Fixpoint rev_app (s1 s2 : string) : string :=
+    match s1 with
+    | "" => s2
+    | String a s1 => rev_app s1 (String a s2)
+    end.
+  Definition rev (s : string) : string := rev_app s "".
+
+  (* Break a string up into lists of words, delimited by white space *)
+  Fixpoint words_go (cur : option string) (s : string) : list string :=
+    match s with
+    | "" => option_list (rev <$> cur)
+    | String a s =>
+       if Ascii.is_space a
+       then option_list (rev <$> cur) ++ words_go None s
+       else words_go (Some (from_option (String a) (String a "") cur)) s
+    end.
+  Definition words : string → list string := words_go None.
+
+  Ltac words s :=
+    match type of s with
+    | list string => s
+    | string => eval vm_compute in (words s)
+    end.
+End String.
diff --git a/tests/ascii.ref b/tests/ascii.ref
new file mode 100644
index 0000000000000000000000000000000000000000..7be9366e465854c532e4c3c2f7f827c28a6c972e
--- /dev/null
+++ b/tests/ascii.ref
@@ -0,0 +1,8 @@
+"a"
+     : string
+"a"%char
+     : ascii
+"a"
+     : ascii
+"a"%stdpp
+     : string
diff --git a/tests/ascii.v b/tests/ascii.v
new file mode 100644
index 0000000000000000000000000000000000000000..54abf45a330874e317dafdc66991576a1b4ae5fb
--- /dev/null
+++ b/tests/ascii.v
@@ -0,0 +1,11 @@
+From stdpp Require Import strings.
+From Coq Require Import Ascii.
+
+Check "a". (* should be string *)
+
+Check "a"%char. (* should be ascii *)
+
+Open Scope char_scope.
+
+Check "a". (* should be ascii *)
+Check "a"%string. (* should be string *)
diff --git a/tests/pretty.v b/tests/pretty.v
index 6bb0768fce926b6a083e3a8f4b6abb633be0f69c..c154908a21664c96e8b99a6655ceaa511a3924d5 100644
--- a/tests/pretty.v
+++ b/tests/pretty.v
@@ -25,8 +25,8 @@ End N.
 Fixed by making the [wp_guard] in [pretty_N_go] proportional to the
 size of the input so that it blocks in case the input is an open term. *)
 Lemma test_no_stack_overflow p n :
-  get n (pretty (N.pos p)) ≠ Some "_"%char →
-  get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char.
+  String.get n (pretty (N.pos p)) ≠ Some "_"%char →
+  String.get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char.
 Proof. intros Hlem. apply Hlem. Qed.
 
 Section nat.
diff --git a/tests/strings.ref b/tests/strings.ref
index 9013eb935c0216264f283f27f7a87cb0d6955838..9be03f81738861857bb9e90e43b0255c35d10827 100644
--- a/tests/strings.ref
+++ b/tests/strings.ref
@@ -1,8 +1,14 @@
+"foo"
+     : string
 "foo"
      : string
 10 =? 10
      : bool
 [10] ++ [12]
      : list nat
-"foo" +:+ "bar"
+("foo" =? "bar")%string
+     : bool
+String.app "foo" "bar"
      : string
+String.app
+     : string → string → string
diff --git a/tests/strings.v b/tests/strings.v
index c88306aacfbd17dbdca7590f2e0c9285a33968d9..82a3e70b803812d2a031b4f84654286ad5c92f7d 100644
--- a/tests/strings.v
+++ b/tests/strings.v
@@ -1,13 +1,22 @@
 From stdpp Require Import strings.
+From Coq Require Ascii.
 
 (** Check that the string notation works without [%string]. *)
 Check "foo".
 
+(** And also with [%string], which should not be pretty printed) *)
+Check "foo"%string.
+
 (** Check that importing [strings] does not override notations for [nat] and
 [list]. *)
 Check (10 =? 10).
 Check ([10] ++ [12]).
 
+Check ("foo" =? "bar")%string.
+
 (** Check that append on strings is pretty printed correctly, and not as
 [(_ ++ _)%string]. *)
 Check ("foo" +:+ "bar").
+
+(** Should print as [String.app] *)
+Check String.app.