aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/bug_7443.v
AgeCommit message (Expand)Author
2020-11-17A reimport of notations now put the corresponding notations again in front.Hugo Herbelin