MLtac2 is a simple library that packages part of the Ltac2 APIs for use in OCaml. It is a partial solution to the discoverability problem in Rocq APIs, providing a simple entry-point for meta-programming in OCaml.
Install MLtac2 through opam:
opam update
opam repo add rocq-released https://rocq-prover.github.io/opam/released/
opam pin add https://github.com/epfl-systemf/mltac2.git