Make hcom, com, coe, et al Chk tactics #393
Description
As it currently stands, the new hcom_chk tactic as given in #386 is the only one with the behavior such that:
- When the boundary is satisfied, don't drop a hole
- When the boundary is unsatisfied, drop a hole around the entire thing
However, when the non-inference hcom is used, you have to do {! hcom ... !} to avoid confusing boundary errors. hcom_chk does this automatically.
The other tactics should replicate this behavior, dropping a hole when the boundary is unsatisfied and automatically removing the cone of silence when the boundary is satisfied.