coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq connecting to other provers

From: Benedikt.AHRENS AT unice.fr
To: Coq Club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] Coq connecting to other provers
Date: Thu, 22 Jan 2009 12:15:22 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

on http://coq.inria.fr/about1-eng.html it says that Coq provides a protocol for connecting with external theorem provers.

I could not find any documentation for this in the reference manual. Could somebody point out for me what I have overlooked, or give me a hint where to find documentation for this feature?

Thanks a lot in advance
ben

[Coq-Club] Transformations under a binder, JAEGER, Eric (SGDN)
- Re: [Coq-Club] Transformations under a binder, Taral
- Re: [Coq-Club] Transformations under a binder, Matthieu Sozeau
  - [Coq-Club] Coq connecting to other provers, Benedikt . AHRENS
    - Re: [Coq-Club] Coq connecting to other provers, Yves Bertot
      - Re: [Coq-Club] Coq connecting to other provers, Thery Laurent