Evidence for https://github.com/coq/coq/issues/15255; build by clone + dune build

dune

(coq.theory
 (name notation_test)

 (flags (:standard)))

dune-project

(lang dune 2.9)
(using coq 0.3)

test1.v

Reserved Notation "L '.=' j" (at level 49, left associativity).

test2.v

(* Fails *)
From notation_test Require Import test1.
(* From notation_test Require Export test1. *)

Reserved Notation "'<obj>_{' L '}' P" (at level 49).

test3.v

(* V1: Works. *)
(* From notation_test Require Import test1. *)
(* Print Grammar constr. *)
(* | "49" LEFTA
  [ SELF; ".="; NEXT ] *)
(* From notation_test Require Import test2. *)
(* Print Grammar constr. *)
(* | "49" LEFTA
  [ SELF; ".="; NEXT
  | "<obj>_{"; term LEVEL "200"; "}"; NEXT ] *)

(* V2: Fails, if test2 doesn't import test1, or if it does. *)
From notation_test Require Import test2.
(* Print Grammar constr. *)
(*
| "49" RIGHTA
  [ "<obj>_{"; term LEVEL "200"; "}"; NEXT ]
*)
From notation_test Require Import test1.