Forked from
Iris / Iris
-
Robbert Krebbers authored
It no longer requires the functions on both sides of the relation to be syntactically the same.
Robbert Krebbers authoredIt no longer requires the functions on both sides of the relation to be syntactically the same.
tactics.v 21.32 KiB