The only documentation of Ltac2 so far is the one in the reference manual: https://coq.inria.fr/refman/proof-engine/ltac2.html
One important point that I want to attract your attention to is the following one: https://coq.inria.fr/refman/proof-engine/ltac2.html#switching-between-ltac-languages
We recommend using the
Default Proof Mode option to switch between tactic languages with a proof-based granularity. This allows to incrementally port the proof scripts.
In particular, calling
Set Default Proof Mode "Classic". will allow you to write some Ltac1 scripts including all the tactics you are used to and
Set Default Proof Mode "Ltac2". will allow you to switch to a fully Ltac2 mode. Even in “Classic” (Ltac1) mode, you can rely on the tactics you have defined using Ltac2 constructs. You can bind them in
A number of tactics are not exported as syntax in the Ltac2 plugin yet: you are encouraged to open issues every time you encounter an example of this. As a workaround, you can use
Ltac2 Notation to redefine the syntax for these existing but unexported tactics.
Thank you for testing Ltac2!