Changes
Page history
Update coq bugs
authored
Mar 06, 2023
by
Ralf Jung
Show whitespace changes
Inline
Side-by-side
coq-bugs.md
View page @
b2d9a79c
...
...
@@ -41,3 +41,4 @@ Priority [HIGH] means that this actively affects how we do things and we have no
*
[
#14513
](
https://github.com/coq/coq/issues/14513
)
(
8.15
)
: Allow
`Global`
on
`Typeclasses Opaque`
/
`Transparent`
and
`Hint Mode`
, inside sections.
*
[
#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
)
\ No newline at end of file