Changes
Page history
Update coq bugs
authored
May 02, 2023
by
Ralf Jung
Show whitespace changes
Inline
Side-by-side
coq-bugs.md
View page @
9f75e971
...
...
@@ -35,6 +35,6 @@ Priority [HIGH] means that this actively affects how we do things and we have no
*
[
#13996
](
https://github.com/coq/coq/issues/13996
)
(
8.14
)
: We should be able to implement
`string_to_ident`
without FFI tricks or
`intros_by_string`
.
*
[
#14548
](
https://github.com/coq/coq/issues/14548
)
(
8.15
)
: Name mangling "light"
*
[
#13969
](
https://github.com/coq/coq/pull/13969
)
(
soon
to be on master): lets us
use mode
`! !`
for
`Reflexive`
*
[
#13969
](
https://github.com/coq/coq/pull/13969
)
(
8.16
)
: lets us hopefully
use mode
`! !`
for
`Reflexive`
*
8.16:
[
reversible coercions
](
https://mattermost.mpi-sws.org/iris/pl/yz8o9mc7apfupy7h7e3h17kqxc
)
*
8.17:
[
future coercion syntax
](
https://github.com/coq/coq/pull/16230
)
\ No newline at end of file
