Update coq bugs authored by Ralf Jung's avatar Ralf Jung
......@@ -4,8 +4,9 @@ Priority [HIGH] means that this actively affects how we do things and we have no
### Ltac vs strings
- [#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.
- [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
......
......