Coq Topic Working Group Meta Programming Rosetta Stone - coq/coq GitHub Wiki

The goal of this working group is to come up with an example for a meta programming / tactic language / plugin implemented in the various common meta programming languages, namely:

OCaml (Enrico)
Ltac (M. Soegtrop) (L. Dubois de Prisque)
Mtac2 (Janno)
Ltac2 (M. Soegtrop)
MetaCoq (L. Dubois de Prisque, K. Maillard)
Elpi (Enrico)

Details (meeting schedule) are TBD.