- All tp_ tactics work without explicit modalities in the goal;
- All tp_ tactics simplify the ghost thread pool points-to;
- Proof term size improvements