aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4882.v
AgeCommit message (Expand)Author
2016-07-01Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).Hugo Herbelin