Changes
Page history
Update coq bugs
authored
May 20, 2021
by
Ralf Jung
Show whitespace changes
Inline
Side-by-side
coq-bugs.md
View page @
5d10d1aa
...
...
@@ -37,3 +37,4 @@ 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 possibly other use-cases).
*
[
#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`
.
*
[
#14208
](
https://github.com/coq/coq/pull/14208
)
(
8.14
)
: Warn on implicitly global
`Instance`
.
*
[
#13725
](
https://github.com/coq/coq/pull/13725
)
(
8.14
)
:
`Global`
on
`Hint Rewrite`
.
\ No newline at end of file
