Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Printing a structured representation of a Prop?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Printing a structured representation of a Prop?


Chronological Thread 
  • From: Enrico Tassi <enrico.tassi AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Printing a structured representation of a Prop?
  • Date: Thu, 2 Jul 2015 09:40:22 +0200

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



Archive powered by MHonArc 2.6.18.

Top of Page