chore: proof mode directory cleanup - #570

Merged

MackieLoeffel merged 28 commits into

leanprover-community:masterfrom

ISTA-PLV:ProofModeFormatting

Aug 7, 2026

Commits on Aug 5, 2026

`InstancesPlainly.lean` and `InstancesUpdates.lean`: multi-trans proofs
alvinylt
committed
4f471de
`InstancesLater.lean`: multi-trans proofs
alvinylt
committed
4b8865e
Minor improvement for `intoLaterN_laterN`
alvinylt
committed
afeb8ec
`Instances.lean`: multi-trans proofs
alvinylt
committed
837696a
`InstancesFrame.lean`: multi-trans proofs
alvinylt
committed
3334192
Format `Tests/Tactics.lean`
alvinylt
committed
cce10b2
Replace all `ϕ` (`\varphi`) with `φ` (`\phi`)
alvinylt
committed
c81ae32
`Tests/Tactics.lean`: comment consistency
alvinylt
committed
ec60b58
Update `proofmode.md`: description about `rw'`
alvinylt
committed
b1beb6f
`Porting.lean`: More descriptive reason for ignoring `iAssumptionCoq`
alvinylt
committed
53f5bf6
Formatting: `iaccu`, `iapply`, `iassumption`, `icases`, `iclear`, `icombine`
alvinylt
committed
de2bc87
Formatting: `ieval`, `iexfalso`, `iexists`, `iframe`, `ihave`, `iinduction`
alvinylt
committed
ba8b2eb
Formatting: `iintro`, `ileft`, `iright`, `iloeb`, `imod`, `ipure`
alvinylt
committed
fa33749
Formatting: `imodintro`, `irename`, `irevert`, `irewrite`, `isplit`, `itrivial`
alvinylt
committed
bb9eb7b
Handle the rest of items in `rocq_tactics.v`
alvinylt
committed
70630eb
Typo fix
alvinylt
committed
6d995a1
Add missing imports: `LazyCoin`, `NondetBool`
alvinylt
committed
1a34a16
Add `rocq_ignore` annotation for `intro_pat.parse_clear`
alvinylt
committed
610e439

Commits on Aug 6, 2026

Commits on Aug 7, 2026