Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Listing all known identifiers, without their types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Listing all known identifiers, without their types


Chronological Thread 
  • 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-----



Archive powered by MHonArc 2.6.18.

Top of Page