Ltac2 in the documentation: https://coq.inria.fr/distrib/current/refman/proof-engine/lta...