blob: f1d4fa789db50ba93bbdd515a8f999e94f8c6e97 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
.. _writing-tactics:
====================
Creating new tactics
====================
The languages presented in this chapter allow one to build complex
tactics by combining existing ones with constructs such as
conditionals and looping. While :ref:`Ltac <ltac>` was initially
thought of as a language for doing some basic combinations, it has
been used successfully to build highly complex tactics as well, but
this has also highlighted its limits and fragility. The experimental
language :ref:`Ltac2 <ltac2>` is a typed and more principled variant
which is more adapted to building complex tactics.
There are other solutions beyond these two tactic languages to write
new tactics:
- `Mtac2 <https://github.com/Mtac2/Mtac2>`_ is an external plugin
which provides another typed tactic language. While Ltac2 belongs
to the ML language family, Mtac2 reuses the language of |Coq| itself
as the language to build |Coq| tactics.
- The most traditional way of building new complex tactics is to write
a |Coq| plugin in |OCaml|. Beware that this also requires much more
effort and commitment. A tutorial for writing |Coq| plugins is
available in the |Coq| repository in `doc/plugin_tutorial
<https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_.
.. toctree::
:maxdepth: 1
../../proof-engine/ltac
../../proof-engine/ltac2
|
