diff --git a/test-normalizer.sed b/test-normalizer.sed
index 5221291174810d3d1d8fc7c7faee6efa9d6cdf53..3f9662bba47b73b0deac50eb948f084345fc0404 100644
--- a/test-normalizer.sed
+++ b/test-normalizer.sed
@@ -6,5 +6,3 @@ s/subgoal/goal/g
 /^File/d
 # extra space removed in https://github.com/coq/coq/pull/16130
 s/= $/=/
-# delete "uses section variable" lines (https://github.com/coq/coq/pull/16208)
-/^[^ ]+ uses section variables? .*\.$/d
diff --git a/tests/notation.v b/tests/notation.v
index b1b3df82c80ce8f08a768e8be791365b1f6e7106..e9b90c89212ade9ea0822d8986b7bdfc0e5372a3 100644
--- a/tests/notation.v
+++ b/tests/notation.v
@@ -1,4 +1,4 @@
-From stdpp Require Import base tactics fin_maps gmultiset.
+From stdpp Require Import base tactics fin_maps gmap gmultiset.
 
 (** Test parsing of variants of [(≡)] notation. *)
 Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
@@ -10,7 +10,9 @@ Proof. naive_solver. Qed.
 
 (** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
 Section map_notations.
-  Context `{FinMap nat M}.
+  (* Avoiding section variables so output is not affected by
+  https://github.com/coq/coq/pull/16208 *)
+  Let M := gmap nat.
 
   Definition test_2 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]} ]}.
   Definition test_3 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]};