aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4287.v
AgeCommit message (Expand)Author
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2015-11-27Univs: entirely disallow instantiation of polymorphic constants withMatthieu Sozeau
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-02Univs: fix test-suite file for #4287, now properly rejected.Matthieu Sozeau
2015-10-02Univs: fix Universe vernacular, fix bug #4287.Matthieu Sozeau