The Coq mailing list

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

Hi all,

In Coq 8.2, the [eq] and [t] fields of the [DecidableType] module type
were declared as "Inline".  I'm not sure how "Inline" is supposed to
work, especially with respect to hint declarations, so I pose below as
simple an example as I can come up with.

First, I have some basic set up code.  I'm specifically interested in
what gets added to the core hint database when the functors below are
instantiated.

<<
  Require Import DecidableType.
  Require Import DecidableTypeEx.
  Require Import FSets.

  Module Functor_fun (E : DecidableType) (Import M : WSfun E).
    Hint Resolve E.eq_refl.
  End Functor_fun.

  Module Functor (M : WS) := Functor_fun M.E M.
>>

With those definitions in hand, I try the following.

<<
  Module Impl := FSetWeakList.Make Nat_as_DT.
  Module Import X1 := Functor Impl.
  Print HintDb core.
>>

Here, [eq_refl] shows up only as a hint for [Nat_as_OT.eq].  Given the
"Inline" declaration in [DecidableType], I would have expected [eq_refl]
to show up as a hint for [eq].

<<
  Module Import X2 := Functor_fun Impl.E Impl.
  Print HintDb core.
>>

Now, [eq_refl] shows up as a hint for [eq].

Appearances suggest to me that the functor instantiations for [X1] and
[X2] should do the same thing, but apparently there is some difference.
 Is this intended to be the case?  What's the difference?

Thanks for any clarification,
Brian