Forked from
Iris / Iris
5400 commits behind the upstream repository.
-
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