... | ... | @@ -2,12 +2,6 @@ |
|
|
|
|
|
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](https://github.com/coq/coq/issues/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](https://github.com/ppedrot/coq-string-ident), 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.
|
|
|
|
|
|
### Typeclasses
|
|
|
|
|
|
- [HIGH] [#5752](https://github.com/coq/coq/issues/5752): `Hint Mode` behaves differently for local context
|
... | ... | |