Arnaud Spiwack
In this article, I started reflecting on my experience designing and implementing a new tactic engine for the Coq proof assistant. Unfortunately I have not finished it and other things took priority. I'm making it available as is hoping it may still contain some useful thoughts.
To build the article, you need to have a Latex distribution installed,
as well as Ocaml (version 3.12 or later) and the melt text processing
tool. The command line to run is ocamlbuild tacengine.pdf
. You can
then find the pdf file in _build/tacengine.pdf
The content of this repository is distributed under Creative Commons licence CC BY 3.0.