aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3723.v
blob: d0b77c451bcb3621b35d9c0192c9226115612042 (plain)
1
2
3
4
5
6
(* Bugs #3787 and #3723 on reinitializing camlp5 levels *)

Definition a := True.
Reserved Notation "-- x" (at level 50, x at level 20).
Reserved Notation "--- x" (at level 20).
Reset a.