diff --git a/tests/notation.v b/tests/notation.v index e9b90c89212ade9ea0822d8986b7bdfc0e5372a3..02ccf06ff3332027a750058b251b59f0d8701fe6 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]};