aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_4771.v
AgeCommit message (Expand)Author
2018-11-12Test case for #4771: Substitution of inline global reference in tactics is br...Maxime Dénès