Documents (TeX, slides etc.) and code for the editor side metaprogramming in Coq.
This provides a simple mechanism to write Emacs editor macros in Coq, using the monadic embedded domain-specific language. We can then run them in Emacs, using the interpreter written in Emacs Lisp.