- Make the ``rewrite /t`` tactic work together with
  :flag:`Universe Polymorphism`.
  This makes tacn:`rewrite` compatible with the HoTT
  library https://github.com/HoTT/HoTT.
  (`#10305 <https://github.com/coq/coq/pull/10305>`_,
  fixes `#9336 <https://github.com/coq/coq/issues/9336>`_,
  by Andreas Lynge, review by Enrico Tassi)