aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_10812.v
AgeCommit message (Expand)Author
2020-05-07Tactic subst now inactive on section variables occurring indirectly in goal.Hugo Herbelin