Hi,

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 `Tactic Notations`

.

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!