coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Clément Pit--Claudel <clement.pit AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Listing all known identifiers, without their types
- Date: Fri, 20 Feb 2015 15:17:34 -0500
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
On 02/20/2015 01:21 PM, Pierre-Marie Pédrot wrote:
> If you can hook in the ideslave interface, there is actually a request
> used by CoqIDE that precisely does that job: this is the duty of the
> "Search" request. Try to read the semi-automatically generated
> documentation echoed by
>
> bin/coqtop -toploop coqidetop --help-XML-protocol
That sound pretty neat! Which version of Coq should I run this with though?
Both 8.4pl2 and trunk say "Don't know what to do with -toploop"
Clément.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1
iQEcBAEBAgAGBQJU55ZeAAoJEC0HUjwO/okMZ48IAI4Wvz9nJ43iWnogkQA60mmX
Lsz1sM/Dmb9GXn/8VCT6ZhI8f6Rgzq8Q27Yv3JwiQHapppxU+HTpuqba9UJioKG4
RwLPZbWIdbafEU13S9nW4uDXH4RlDFxKADK9ErWNI+cqoD7oz6DbPX1mM0va4VF5
3i85ghcohvG306UrIKtUgnchWztV8K76rmBO9+WTGvgtPDUuPlp7zfinf+SD1EUP
mZBxr0vi16v2wnUhToaLZEOLU2vX6jBBWFcVkXPirakeWdC7qMnboh89YB5/Ne1A
eSQnvUHyqFk+Nbye0LL81FrsRyAJpN7Uhg1N8zi2vKntzss8z3WrdU/PZ4budNY=
=SyIC
-----END PGP SIGNATURE-----
- [Coq-Club] Listing all known identifiers, without their types, Clément Pit--Claudel, 02/19/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Abhishek Anand, 02/19/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Clément Pit--Claudel, 02/20/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Pierre-Marie Pédrot, 02/20/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Clément Pit--Claudel, 02/20/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Pierre-Marie Pédrot, 02/20/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Clément Pit--Claudel, 02/20/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Pierre-Marie Pédrot, 02/20/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Clément Pit--Claudel, 02/20/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Pierre-Marie Pédrot, 02/20/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Clément Pit--Claudel, 02/20/2015
- Re: [Coq-Club] Listing all known identifiers, without their types, Abhishek Anand, 02/19/2015
Archive powered by MHonArc 2.6.18.