Priority [HIGH] means that this actively affects how we do things and we have not found a workaround. For [MEDIUM] we have an acceptable workaround or accounted for it sufficiently by changing our design. The rest is [LOW].
Ltac vs strings
[HIGH] #7922: Cannot convert between strings and identifiers in Ltac, leading to horrible code and lots of hacks all over the place.
There is a prototype plugin, but it doesn't compile any more and also it never worked very well: let x = "foo" in ident_of_string x was not supported.
[HIGH] #5752: Hint Mode behaves differently for local context
[HIGH] #9058: Hint Mode cancels entire search too early. For this reason we cannot use Hint Mode Equiv ! : typeclass_instances, so we suffer from backtracking and loops whenever Equiv ? comes up.
[HIGH] #7916: Cannot set mode for Reflexive because setoid_rewrite makes some strange queries, so we suffer from backtracking and slow rewriting whenever Reflexive ? comes up.
[MEDIUM] #6714: Set Typeclasses Unique Instances does not have any (or at least not the expected) effect. Work-around: Class NoBackTrack.
[MEDIUM] #7914: TC resolution is unable to use the fact that Prop is a subtype of Type. Work-around: Have a separate typeclass IntoPureT that uses refine through a Hint Extern.
[MEDIUM] #6583: apply triggers TC resolution on unrelated goals so proof mode tactics randomly fail when the user has other typeclass goals open. Work-around: Use typeclasses eauto instead of apply _ and otherwise notypeclasses refine instead of apply. It's hard to tell if we got this all right, though, and it may not just be apply that does this.