Skip to content

Ltac2 Tuto Matching: Add discussion matching letin + fix typos#128

Merged
thomas-lamiaux merged 2 commits into
rocq-prover:mainfrom
thomas-lamiaux:add-ex-letin-matching
Apr 28, 2026
Merged

Ltac2 Tuto Matching: Add discussion matching letin + fix typos#128
thomas-lamiaux merged 2 commits into
rocq-prover:mainfrom
thomas-lamiaux:add-ex-letin-matching

Commits

Commits on Apr 28, 2026