Mtac as a Plugin
Typed Tactics for Coq 8.5
Copyright (c) 2015 Beta Ziliani firstname.lastname@example.org
Based on Mtac 1.2, with contributions from Jan-Oliver email@example.com.
Distributed under the terms of the MIT License, see LICENSE for details.
This archive contains the intepreter of Mtac as a plugin.
The archive has 3 subdirectories:
src contains the code of the plugin in mtac.ml4, and the interpreter in run.ml. theories contains support Coq files for the plugin. Mtac.v declares the plugin on the Coq side, and the main inductive type for Mtac. Hash.v is a hash-table, and Mtactics.v contains some useful tactics. test-suite contains files testing the different features of Mtac.
The plugin works currently with Coq v8.5. Through OPAM, this plugin is available in Coq's development repository:
opam repo add coq-released https://coq.inria.fr/opam/released opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev opam install -j4 -v coq:mtac
Otherwise, you should have coqc, ocamlc and make in your path. Then simply do:
To generate a makefile from the description in Make, then
This will consecutively build the plugin, the supporting
theories and the test-suite file.
You can then either
make install the plugin or leave it in its
current directory. To be able to import it from anywhere in Coq,
simply add the following to
Add LoadPath "path_to_mtac/theories" as Unicoq. Add ML Path "path_to_mtac/src".
Once installed, you can
Require Import Mtac.Mtac to load the
plugin. The plugin defines the following option to execute a
run t as htaking Mtactic t and defining h as the result of the execution of the tactic in the local environment.
rrun ttaking Mtactic t and refining the current goal with the result of the execution of the tactic.
Mrun tto execute Mtactic t as part of a term.