blob: b82de1a879b0ac1eafd0bb47bf05eb8c2c6b4c72 (
plain)
1
2
3
4
5
6
7
|
- 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)
|
