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

Section foo.
  Global Arguments foo / .
End foo.