Remove all `ProofScript` sequent features - #3284

Draft

brianhuffman wants to merge 13 commits into

Commits on Jun 15, 2026

saw-script: Remove all sequent-specific `ProofScript` tactics.
brianhuffman
committed
31fa6aa
saw-script: Remove `enable_sequent_goals`, `disable_sequent_goals`.
brianhuffman
committed
e7e789f
saw-central: Remove always-false field `rwSequentGoals`.
brianhuffman
committed
f865278
saw-central: Remove dead code from Proof.hs.
brianhuffman
committed
afd95b7
saw-central: Remove unused constructors from `Evidence`.
brianhuffman
committed
71d014f
saw-central: Remove unused local-hyps argument from `RewriteEvidence`.
brianhuffman
committed
967232e
saw-central: Remove `RawSequent`, `FocusedBranch` and `SequentState`.
brianhuffman
committed
f79b62b
saw-central: Remove type `Sequent` in favor of `Prop`.
brianhuffman
committed
0a802f6
saw-script: Add `specialize_thm`, a pure variant of `specialize_theorem`.
brianhuffman
committed
9c9f4be
Add new SAWScript primitive `term_thm : Term -> Theorem`.
brianhuffman
committed
d0f24ce
Add new SAWScript primitive `apply_thm`.
brianhuffman
committed
9bf3b69
Add new reimplementation of SAWScript primitive `goal_insert`.
brianhuffman
committed
0f1bf1b
Add command `subproof : ProofScript () -> ProofScript ()`.
brianhuffman
committed
2f1bf3d