Changes
Page history
Update coq bugs
authored
Nov 25, 2021
by
Ralf Jung
Show whitespace changes
Inline
Side-by-side
coq-bugs.md
View page @
d764af48
...
...
@@ -36,5 +36,6 @@ Priority [HIGH] means that this actively affects how we do things and we have no
*
[
#13265
](
https://github.com/coq/coq/pull/13265
)
(
8.13
)
: using
`v closed binder`
for
`WP`
notation (and other use-cases like big-ops).
*
[
#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`
.
*
[
#13725
](
https://github.com/coq/coq/pull/13725
)
(
8.14
)
:
`Global`
on
`Hint Rewrite`
.
*
[
#13654
](
https://github.com/coq/coq/issues/13654
)
(
8.14
)
: custom entry import fixed
*
[
#14548
](
https://github.com/coq/coq/issues/14548
)
(
8.15
)
: Name mangling "light"
*
[
#14513
](
https://github.com/coq/coq/issues/14513
)
(
8.15
)
:
`Global`
on
`Typeclasses Opaque`
/
`Transparent`
.
\ No newline at end of file
