Ltac2
A standalone implementation of Ltac2 as a Coq plugin. Now part of the main Coq repository.
Install / Use
/learn @rocq-prover/Ltac2README
Archived repository of Ltac2
Ltac2 source code has moved to the Coq repository. The other branches in this repo contain the source code for Coq versions before 8.11, but they are not maintained anymore. These versions can also be accessed through opam or the Windows installer of Coq (starting with 8.8.2).
View on GitHub75/100
Security Score
Audited on Feb 20, 2026
No findings