The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

We are proud to announce the official 1.0 release of Mtac2.

A little FAQ:

1. What is it?
   It is a plugin providing Coq with a typed tactic language. It is described in this paper.

2. Can you give a quick example?
   For instance, in a recent email someone got bitten by Ltac’s lack of support for coercions. In Mtac2, the terms you write are Coq’s terms, as Coq understands them.

   Definition show_H:=
    match_goal with
    | [[? (O:ordType) (x y : O) (G:Prop) | (H: x == y) |- G]] => M.print_term H
    end.
   

   Of course, the price to pay is that you need to provide the typing information. But once you write it down, you know it works!

   Much more can be found in Mtac2’s github page.

3. Is there an opam archive?
   We just created the PR for Coq’s opam’s archive. Once its processed it should be available simply typing opam install coq-mtac2.

4. Which version of Coq does it support?
   Currently only 8.7.X, but we plan to add 8.8 soon. Feel free to ask!

5. Why the 2 in the name? Why not Mtac 2.0?
   We wanted to make clear that there is much more to Mtac2 than what there was in Mtac. So if you’ve heard about Mtac, and its limitations, take a new look at Mtac2, it has a lot more to it.

6. I heard about some MetaCoq, is it related?
   Yes, MetaCoq was the name for Mtac2 before we decided that the name didn’t really express what Mtac2 is. Actually, the first project Mtac should’ve been named MetaCoq, since it only provides meta-programming and not tactic programming in full.

The Mtac2’s team.