summaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened/3071.v
blob: 611ac6065571eb9300a08083c3d409b7cbefb4cd (plain)
1
2
3
4
5
Definition foo := True.

Section foo.
  Global Arguments foo / .
Fail End foo.