From c4055887b620efc04310e73e4f8682ae6cad1b73 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 27 Jun 2022 07:59:09 -0400
Subject: [PATCH] avoid section variables in printed terms

---
 test-normalizer.sed | 2 --
 tests/notation.v    | 6 ++++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/test-normalizer.sed b/test-normalizer.sed
index 52212911..3f9662bb 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 b1b3df82..e9b90c89 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]};
-- 
GitLab