- **Changed:**
  Internal definitions generated by :tacn:`abstract`\-like tactics are now inlined
  inside universe :cmd:`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).