Skip to content

Fix syntax and parsing examples in tutorial_ltac2 - #133

Merged
thomas-lamiaux merged 2 commits into
rocq-prover:mainfrom
amblafont:patch-1
Aug 14, 2026
Merged

Fix syntax and parsing examples in tutorial_ltac2#133
thomas-lamiaux merged 2 commits into
rocq-prover:mainfrom
amblafont:patch-1

Update tutorial_ltac2_for_ltac1_users.v

1d23ca1
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

12 warnings
build
succeeded Aug 14, 2026 in 4m 23s