The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

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 ?

-- 

Jacques-Henri Jourdan