The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi all,

Is there a way to list all identifiers known to Coq, without printing their 
type? Something similar to the output of [SearchPattern _], but with type 
information stripped out. That is, a way to get

    Mult.mult_plus_distr_l
    Mult.mult_succ_l
    Mult.mult_succ_r
    Mult.odd_even_lem
    Mult.mult_acc_aux

instead of

    Mult.mult_plus_distr_l: forall n m p : nat, n * (m + p) = n * m + n * p
    Mult.mult_succ_l: forall n m : nat, S n * m = n * m + m
    Mult.mult_succ_r: forall n m : nat, n * S m = n * m + n
    Mult.odd_even_lem: forall p q : nat, 2 * p + 1 <> 2 * q
    Mult.mult_acc_aux: forall n m p : nat, m + n * p = Mult.mult_acc m p n

I've pushed a basic implementation of such a feature to 
https://github.com/cpitclaudel/coq/commit/198b9c47dedf4fa3b2a95ab7102b2d2d4ada392f
 (it adds an option "Search Minimal", which when activated reduces the output 
of search commands to just names). It would be nice to have that feature in 
Coq, though! But perhaps I missed an existing option? Another possible 
direction would be to implement a [Dump Identifiers To File <path>] command, 
which would write all names to a separate files.

A bit of context: such a command would be useful to get better completion 
support for Coq in Emacs: using the list of all known terms and theorems one 
could implement a nice autocompletion package. Unfortunately ProofGeneral 
currently has trouble dealing with the output of [SearchPattern _] when large 
libraries are loaded (e.g. Reals), because it uses regular expressions to 
find the next prompt (in my experiments, reading the full list of all defined 
terms with their types takes about 3s; patching PG to do a plain string 
search first takes it down to about 1.5s; without the types, it takes 50ms).

Thanks!
Clément.