A standalone implementation of Ltac2 as a Coq plugin. Now part of the main Coq repository. - View it on GitHub