Forked from
Iris / stdpp
1857 commits behind the upstream repository.
-
Robbert Krebbers authored
This avoids `naive_solver` tearing whole goals apart, even if the goal appears exactly as a hypothesis.
Robbert Krebbers authoredThis avoids `naive_solver` tearing whole goals apart, even if the goal appears exactly as a hypothesis.
tactics.v 24.01 KiB