... | ... | @@ -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
|
|
|
|
... | ... | |