The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

According to this bug report, 
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2815, 
SearchAbout is broken for non-file modules.

On 03/14/2013 03:54 PM, Jacques-Henri Jourdan wrote:
> Hi coq-club !
>
>
> SearchAbout does not give all the interesting results in the module Z :
>
>
>
> Welcome to Coq 8.4pl1 (January 2013)
>
>
> Coq<  Require Import ZArith.
> [Loading ML file z_syntax_plugin.cmxs ... done]
> [Loading ML file quote_plugin.cmxs ... done]
> [Loading ML file newring_plugin.cmxs ... done]
> [Loading ML file omega_plugin.cmxs ... done]
>
>
> Coq<  SearchPattern (Z ->  Z ->  Z).
> Zmod': Z ->  Z ->  Z
>
>
> Coq<  Check (Z.add).
> Z.add
> : Z ->  Z ->  Z
>
>
> Do you have any idea why ?