aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/NotationsCoercions.v
AgeCommit message (Expand)Author
2020-11-21Fixes #13432: regression with notations involving coercions caused by #11172.Hugo Herbelin