aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_10060.v
AgeCommit message (Collapse)Author
2019-11-05Forbid Include inside sectionsGaƫtan Gilbert
This probably does not work well in general, and specifically avoids an anomaly fixing https://github.com/coq/coq/issues/10060