diff options
Diffstat (limited to 'doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md')
| -rw-r--r-- | doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md deleted file mode 100644 index e0573a2c74..0000000000 --- a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md +++ /dev/null @@ -1,4 +0,0 @@ -- Internal definitions generated by abstract-like tactics are now inlined - inside universe Qed-terminated polymorphic definitions, similarly to what - happens for their monomorphic counterparts, - (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot). |