The Coq mailing list

["Brian E. Aydemir" <baydemir AT cis.upenn.edu>]

Hi everyone,

I'm a little confused about how Modules and Hints interact.  The  
following example illustrates my problem.

(* ***************** *)
Module Type FOO.
  Parameter P : nat -> Prop.
  Axiom P_true : forall n, P n.
  Hint Resolve P_true.
End FOO.

Declare Module Foo : FOO.

Theorem baz : forall n, Foo.P n.
info auto. (* why is P_true in the hints database here? *)
Qed.
(* ***************** *)

In the proof of baz, I was expecting that "P_true" would _not_ be in  
the Hints database.  Print HintDb and the behavior of auto say that  
I'm wrong.  (I would expect, however, that if I had done Import Foo,  
then P_true would be in the database.)

My questions now:

[1] Suppose that I'm not allowed to change FOO.  Is there some way I  
could have declared Foo such that P_true would _not_ end up in the  
Hints database.

[2] Is the behavior I'm seeing actually the intended behavior?  I  
thought the reference manual said that this shouldn't actually  
happen, but I can't seem to find the spot where I might have read that.

Thanks for any help,
Brian