diff options
| author | Pierre-Marie Pédrot | 2019-07-03 17:26:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-08 20:48:07 +0200 |
| commit | 0b2b3e2baa3e004bf937ea001635b47ed781c9db (patch) | |
| tree | 0af667789f3f7eaf99e3801570a6efb45b91595e | |
| parent | d929838be77e30db04cd91201542bb52ed3ff7fd (diff) | |
Adding a changelog.
| -rw-r--r-- | doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md | 4 |
1 files changed, 4 insertions, 0 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 new file mode 100644 index 0000000000..e0573a2c74 --- /dev/null +++ b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.md @@ -0,0 +1,4 @@ +- 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). |