We present Actema, a prototype of user interface where formal proofs can be built through gestural actions, and its integration within Coq through the coq-actema plugin. The latter relies on a client-server architecture, where the plugin requests proof steps from the interface, which are then compiled to appropriate tactic calls. To avoid cluttering the proof script with these calls, graphical proofs are stored separately on disk, and recompiled upon execution of the script. This should also allow to “replay” proofs visually in the interface, which is vital for readability and maintenance. The plugin is usable with any Coq IDE, and its design adapted to any goal-directed interactive theorem prover supporting intuitionistic first-order logic.