Closed SkySkimmer closed 1 year ago
x : y as a ltac pattern was equivalent to x and will be removed in https://github.com/coq/coq/pull/16798
x : y
x
This is ready to merge
OK, will merge after observing CI (may need to adjust compatibility).
x : y
as a ltac pattern was equivalent tox
and will be removed in https://github.com/coq/coq/pull/16798