coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Printing a structured representation of a Prop?
Date: Wed, 01 Jul 2015 21:30:32 -0700

Hi Tej,

On 06/30/2015 05:24 AM, Tej Chajed wrote:
> As far as launching coqtop with ideslave in trunk, this works for me but I
> don't understand the new async proofs protocol (I picked the control
> channel port randomly):
> coqtop -main-channel stdfds -control-channel 127.0.0.1:60875
> <http://127.0.0.1:60875> -ideslave -async-proofs on

Did you get it to answer a query at all?

Re: [Coq-Club] Printing a structured representation of a Prop?, (continued)
- Re: [Coq-Club] Printing a structured representation of a Prop?, Enrico Tassi, 07/01/2015
  - Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/02/2015
    - Re: [Coq-Club] Printing a structured representation of a Prop?, Valentin Robert, 07/02/2015
      - Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/02/2015
    - Re: [Coq-Club] Printing a structured representation of a Prop?, Enrico Tassi, 07/02/2015
- Re: [Coq-Club] Printing a structured representation of a Prop?, Clément Pit--Claudel, 07/02/2015