From 45fd520d555e9d9bfa3d3894ae66079fbbce17f0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 28 Jun 2022 08:32:01 -0400
Subject: [PATCH] avoid section variables for real
---
tests/notation.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tests/notation.v b/tests/notation.v
index e9b90c89..02ccf06f 100644
--- a/tests/notation.v
+++ b/tests/notation.v
@@ -12,7 +12,7 @@ Proof. naive_solver. Qed.
Section map_notations.
(* Avoiding section variables so output is not affected by
https://github.com/coq/coq/pull/16208 *)
- Let M := gmap nat.
+ Notation 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