Skip to content

Tutorial Ltac2 for Ltac1 users#131

Merged
thomas-lamiaux merged 17 commits into
rocq-prover:mainfrom
thomas-lamiaux:tuto-Ltac2forLtac1
May 17, 2026
Merged

Tutorial Ltac2 for Ltac1 users#131
thomas-lamiaux merged 17 commits into
rocq-prover:mainfrom
thomas-lamiaux:tuto-Ltac2forLtac1

Update src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v

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

Annotations

12 warnings
build
succeeded May 17, 2026 in 4m 0s