The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, Jul 01, 2015 at 09:29:31PM -0700, Clément Pit--Claudel wrote:
> Thanks for this pointer. I have no idea what the parameter to
> print_adt is, however. Is it connected to the PrintAst constructor in
> ide.ml?

I guess the best documentation is the underlying API in stm/stm.mli.
When CoqIDE sends a sentence to Coq is performs an "add" call.
The result is a unique id (called Stateid.t).  print_ast takes this
id and prints the AST of the sentence corresponding to that id.

The best way to see how the protocol works is to start CoqIDE with
-debug and look at the debugging output in the terminal.  There is much
more than the protocol, but there is no better way.  The messages are
also documented in ide/interface.mli IIRC.

I told you you should have come to the CoqCS ;-P
-- 
Enrico Tassi