summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4708.v
blob: ad2e5810043acaf30a496abef85b6de54c699baf (plain)
1
2
3
4
5
6
7
8
(*Doc, it hurts when I poke myself.*)

Notation "'" := 1. (* was:
Setting notation at level 0.
Toplevel input, characters 0-18:
> Notation "'" := 1.
> ^^^^^^^^^^^^^^^^^^
Anomaly: Uncaught exception Invalid_argument("index out of bounds"). Please report. *)