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 @
b4522fbd
...
...
@@ -36,6 +36,5 @@ 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`
*
8.15:
`#[projections(primitive=yes/no)]`
for better primitive projection control.
*
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