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