Coq 8.11.0 released, featuring new Ltac2 tactic language (github.com)

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