Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
This avoids weird Ltac behaviors like those in !272. Also, change `before_tc` keyword into `as` to be consistent with other tactics.
Robbert Krebbers authoredThis avoids weird Ltac behaviors like those in !272. Also, change `before_tc` keyword into `as` to be consistent with other tactics.
