The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 20/02/2015 19:17, Clément Pit--Claudel wrote:
> It's an interesting fallback, but it doesn't have the flexibility
> that I'm looking for; in particular, it doesn't tell you which
> commands are accessible at a given point in a proof, and under which
> name (depending on what you [Require Import], symbols may be
> available under different names).

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

PMP

Attachment: signature.asc
Description: OpenPGP digital signature