See the attached example file.  This is very rudimentary, only
supporting session evaluation and without support for smart translation
between Org-mode and Coq data structures.

See the attached example file.