A small tutorial for Ocaml plugins to extend the Coq system

This example was sent to me by Matej Kosik, in preparation for a Coq Implementors Workshop. (* ————————————————————————– *) (* *) (* Initial ritual dance *) (* *) (* ————————————————————————– *) DECLARE PLUGIN “demo” (* Use this macro before any of the other Ocaml macros. Each plugin has a unique…

Continue reading