aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_9313.v
AgeCommit message (Collapse)Author
2019-02-04Enrich implicits for instancesJasper Hugunin
For compatibility, also * Adjust implicits on equiv_transitivity and equiv_symmetry, and in some closed bugs * Add overlay for HoTT setting Arguments on some instances.