blob: 4dc0bead7b1b269db9bdc0657c22dd8e9f7bdddd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(* Similar to #9521 (was an anomaly unknown level 150 *)
Module A.
Declare Custom Entry expr.
Notation "p" := (p) (in custom expr at level 150, p constr, right associativity).
Notation "** X" := (X) (at level 200, X custom expr at level 150).
Lemma t : ** True.
Abort.
End A.
(* Similar to #9517, #9519, #11331 *)
Module B.
Declare Custom Entry expr.
Notation "p" := (p) (in custom expr at level 100, p constr (* at level 200 *)).
Notation "** X" := (X) (at level 200, X custom expr at level 150).
Lemma t : ** True.
Abort.
End B.
|
