A Blog for the CoqHoTT project. Informal posts about Homotopy Type Theory and the Coq Proof Assistant.

Rss feed
February 14, 2016

This post describes the new tactic engine designed by Arnaud Spiwack which has replaced the old implementation beginning from Coq 8.5. To replace this work in its context, we first recall the history of tactics in Coq, both from the point of view of the user and the developer. There will be more OCaml code than Coq code, so please bear with me. Hopefully this will clarify things up for people outside of the cénacle of Coq developers, and provide hindsights into the current design choices.

read more
February 5, 2016


read more